Eclipse Community Forums: Modeling (top-level project) » The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints.

Home » Modeling » Modeling (top-level project) » The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints.

Show: Today's Messages :: Show Polls :: Message Navigator

The most suitable theorem prover/validation tool for eclipse to validate OCLineCORE constraints. [message #1837839]

Mon, 08 February 2021 13:34

houda houda

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.

Report message to a moderator

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

Ed Willink

Messages: 7506
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

Report message to a moderator

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

houda houda

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.

Report message to a moderator

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

Ed Willink

Messages: 7506
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

Report message to a moderator