Hi,

You may want to look at the article entitled "Behavioral Interface Specification Languages" by Hatcliff, et al. in ACM Computing Survey June, 2012. Then take a look at JML and the progress made by Gary Leavens' group at Univ. of Central Florida.

Good luck!

For a practial approach I would take a look at the work from Daniel Ratiu, like "

Language engineering as an enabler for incrementally defined formal analyses". In the context of the mbeddr project he integrated formal analyses in state machine (and other stuff). Very cool, real, appliable.

The main issues with Formal Techniques (FM is a subset) are:

- Notational barrier: models must be readable by "normal" engineers and managers. While the mathematical notation is compact, it is not enough standardised and it requires too many detailed statements that could be filled in in the back. Using some pre-defined ASCII strings would already help. Make it look more like a programming language and automate the generation of the plumber code.

- Lack of support for real concurrency. (the main one at the time was CSP with FDR as model checker but this has lost popularity).

I am a strong believer in FM since we tried it out for developing anew a distributed RTOS. The biggest gain was actually in the design phase with as a result that the final code size was 10x smaller. But to reach widespread adoption, the entry barrier will have to be considerably owe red. It is also wrong to say the FMs are mainly to verify e.g. source code. At that moment, using FM is like using an extended static checker. If the model was wrong (relative to specs) it might be proven right in syntax but not in semantics.

I'm not sure how far my research is related to 'formal' MDD, but I'm looking into model-driven development of information systems. Here the issue is model evolution along with schema evolution and data evolution of the database. Especially data evolution is a problem, for example because of semantic information that are not defined in the model. So any tool that can properly generate complete data evolution code from a semantically rich model would be highly appreciated by many, I believe.

Another issue that I NEVER saw discussed in research is what happen if a buggy model was used to create data and how the data can be (automatically) fixed when a fix to the model is available. This is a ubiquitous problem in practice but pretty much completely ignored in research.

Also, if you can be interested in formalizing semantic information related to a model, you may look at my paper "Optimising Conceptual Data Models through Profiling in Object Databases", which in effect uses the semantic information that is created by users when they use an information system and uses this to indicate semantic problems and performance problems in data models. All this is done using model-driven development techniques.

Another problem related to MDD of information systems is the issue of embedded objects (second class objects), which have different schema characteristics than normal objects. These are not discussed in research either but are often used in industry.

One final explanation: In information systems I often refer to object databases. They are often considered 'old' or even 'dead', but they are in reality common in certain industries such as aviation and defense industries.

Also I hope object databases will become fashionable again because of numerous advantages that they have over relational databases when used in agile development project, such as ease of model evolution.

Finally, what is important for MDD, in objects databases the conceptual model is virtually equivalent to the physical/logical model.

Hi

MDD means dealing with differents models of a system at differents levels of abstraction. At each level it is sometimes necessary to prove properties about the system using the corresponding model of the system at this level (invariants, persistence, safety, liveness properties and fairness conditions). For verification purpose one can use formal methods. Some limitations such as state explosion problems exist but new techniques allow to use abstractions.

For me quite interesting topic is applications of category theory in model-driven engineering. Diskin gives good introduction to possible benefits.

One important area is test case generation from uml diagrams

I was involved in a European project called DEPLOYED where the objective was to help Industry partners integrate Formal methods development techniques and tools in their development process. Conversely, the project also helped research partners in fine tuning their formal methods and tools to address Industry pilot cases. The main methods put forward in the project were Event-B but others were addressed.

In the DEPLOY project, my research center CETIC was involved in the collection of evidence related to achievement made by these Industry pilots as well as other effort.

I can suggest that you take a look at http://www.fm4industry.org which resulted from the project and present various achievements from the project.

With regards to formal method development, one of the most challenging part to dramatically improve their Industry take-up is to integrate a complete chain of tools. Currently, very few examples exist where formal models can automatically lead to the generation executable proven correct code. I know of Siemens Transport System that used B (not event B) to generate Subway controller of the driver-less subway line in Paris among others. This example is presented at the website mentioned above.

The pilot on test case generation from a UML-like workflow notation from SAP is also explained at this website.

The main problem is that if you only use formal method here and there, then the final results can not be proven correct and a heavy testing effort remains required. The formal models are then just another complex artifact to maintain throughout the system and software life cycle (development, maintenance, evolution until retirement).

If you undertake Industry pilots as part of you research please consider contributing your pilot results to the wiki above.