Projects on Formal Methods and Semantics of Concurrent Systems (MFPAR/ConForM)

The project is directed towards the development of concurrent or distributed systems. It is well accepted that the development of large and complex systems needs appropriate methods. The use of formal techniques as well as supporting tools are key for managing their inherent complexity. This project proposes a formal specification language called CO-OPN: Concurrent Object Oriented Petri Nets. Behavioural concurrency aspects are supported by algebraic nets while data-structures are modelled by algebraic abstract data types. Tools have been built to support this formalism and are namely a graphical editor, a compiler, and a simulator for prototyping specifications. This environment, called SANDS for Structured Algebraic Net Development System, also supports analysis techniques such as the proof of branching time temporal logic formulae over CO-OPN specifications.

Description of the EU Esprit project DeVa (20072) (Design for Validation)

Directory of Formal Specification Projects

• General description of the project
  • Semantics of a concurrent object oriented specification language
  • Tools supporting the development of formal specifications
  • Temporal analysis techniques for formal specifications
  • Methodology for producing parallel probabilistic algorithms from abstract formal specification
  • Specification compiler for MIMD machines
• Formal specification case studies
• References
• Object-oriented formal techniques

Contact : Didier Buchs and also the members of MFPAR/ConForM