Skip to main content


Eclipse Community Forums
Forum Search:

Search      Help    Register    Login    Home
Home » Modeling » Modeling (top-level project) » The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints.
The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints. [message #1837839] Mon, 08 February 2021 13:34 Go to next message
houda houda is currently offline houda houdaFriend
Messages: 12
Registered: February 2021
Junior Member
Hello,

I would like to apologize in advance if the forum is not appropriate for my topic ( redirect me to the appropriate one if possible).

I'm working on a model to model transformation, using ECORE metamodels and OCL constraints. I would like to know What is the best theorem prover/ testing tool (exp: coq, USE..) that I can use with Eclipse (as a plug-in or so) to express/validate mathematically the proposed OCL constraints that are embedded in my Ecore model?
I found coqoon which is an Eclipse plugin providing a feature-complete development environment for Coq projects. However, after little research I found out that it was not updated to be compatible with recent Coq versions, so I hesitated.

Thank you.

Re: The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints [message #1837860 is a reply to message #1837839] Mon, 08 February 2021 19:57 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 7176
Registered: July 2009
Senior Member
Hi

The OCL forum is more appropriate.

Eclipse OCL and USE are indeed the two main OCL implementations, bud sadly they lack compatibility beyond a superficial compliance with the same OCL syntax. USE is a kind of OCL 1.x++ while the Classic Eclipse OCL is OCL 2.4-- and Pivot Eclipse OCL is OCL 2.'next'.

USE is a self-contained framework. This has many advantages, but means that there is no Eclipse compatibility and AFAIAA Ecore compatibility has been a top user request for many years. USE is for UML-based OCL.

OCL related proofs is IMHO a much neglected research topic with many of the research papers seeming to seek to prove that OCL is is sound rather than that a suite of user OCL constraints are 'useful' or more importantly what is unsound.

While using Eclipse, EMF and Eclipse-based OCL, the EMF2CSP project is perhaps your best bet at some related proof technology.

However my work on model transformation leads me to realize that metamodels define a very restrictive type system that drastically reduces the search space for legal solutions. My subjective observations from the side lines lead me to suspect that many of the transformations from e.g. OCL to Alloy or Coq throw away the stengths of the metamodels and so lead to tools that take forever to reason about unrealistically small models. If my stack of to-dos wasn't already overflowing I would love to look at a direct metamodel-driven OCL approach to OCL proofs.

Regards

Ed Willink
Re: The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints [message #1838048 is a reply to message #1837860] Sun, 14 February 2021 19:17 Go to previous messageGo to next message
houda houda is currently offline houda houdaFriend
Messages: 12
Registered: February 2021
Junior Member
Hello Ed,
Thank you for the quick and very insightful response, I am very appreciated for that.
I took a look into EMFtoCSP project and it seems like a useful solution for my problem.
However, by taking a look into the project's GitHub (available at https://github.com/SOM-Research/EMFtoCSP ), it seems as if the project had not been updated for several years, which makes me wonder, is it outdated? or is it still a valid tool to be considered for ongoing research projects?

Regards.
Re: The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints [message #1838058 is a reply to message #1838048] Mon, 15 February 2021 06:03 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 7176
Registered: July 2009
Senior Member
HI

Sadly few research projects survive the duration of the original student's PhD. Each research student often starts again and discards again. I have offered to host a few OCL add-ons as part of Eclipse OCL, but few students are interested or able to commit enough time to provide the initial contribution which must satisfy Eclipse IP no copying rules.

Bottom line. Be grateful to GitHub, you t least have a starting point from which to reactivate.

Regards

Ed Willink
Re: The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints [message #1838072 is a reply to message #1838058] Mon, 15 February 2021 12:04 Go to previous messageGo to next message
houda houda is currently offline houda houdaFriend
Messages: 12
Registered: February 2021
Junior Member
Hello Ed.
Thank your for your detailed answer. I appreciate it.

Best regards!
Re: The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints [message #1840657 is a reply to message #1838072] Wed, 21 April 2021 13:45 Go to previous message
Ed Willink is currently offline Ed WillinkFriend
Messages: 7176
Registered: July 2009
Senior Member
Message deleted. Posted to wrong list.

[Updated on: Wed, 21 April 2021 14:20]

Report message to a moderator

Previous Topic:Operational analysis users capture
Goto Forum:
  


Current Time: Mon Jun 21 01:25:34 GMT 2021

Powered by FUDForum. Page generated in 0.01947 seconds
.:: Contact :: Home ::.

Powered by: FUDforum 3.0.2.
Copyright ©2001-2010 FUDforum Bulletin Board Software

Back to the top