MORSE: Methods and Tools for the Formal Verification of Critical Embedded Interoperable Systems

Recent news

• 16/07/2006:
  • New documents (private zone)
• 12/06/2006:
  • New documents (private zone)
  • REE paper on MORSE (in french)
• 10/05/2006:
  • New documents (private zone)
• 23/12/2005:
  • New documents (private zone)
  • New deliverable in the "deliverable space" (protected access)
• 10/12/2005:
  • New documents (private zone)
  09/09/2005:
  • New documents (private zone)
• 11/07/2005:
  • New documents (private zone)
• 08/07/2005:
  • New documents (private zone)
• 30/06/2005:
  • New documents (private zone)
• 10/01/2005:
  • New documents (private zone)
• 31/12/2004:
  • New documents (private zone)
  • New deliverable in the "deliverable space" (protected access)
• 16/07/2004:
  • New documents (private zone)
• 10/07/2004:
  • New documents (private zone)
  • New publications
• 13/04/2004:
  • New documents (private zone)
• 01/04/2004:
  • New documents (private zone)
• 09/02/2004:
  • Minutes of the feb 6, 2004 meeting (private zone)
• 26/01/2004:
  • First semester deliverable in the "deliverable space" (protected access)
• 26/12/2003:
  • Minor updates(in private zone), first document in deliverable zone (to be validated)
  • Added the latex template (as a ready-to-use package)
• 21/12/2003:
  • Restructuration of the private zone according to the 19/12/2003 meeting's descisions
  • added the "fournitures" zone (empty)
  • English version of public pages added

Introduction

The objective of the MORSE project is to provide a solution for the development of certifiable industrial applications in the field of avionics, and more specifically for drones. This class of applications is characterized by the following constraints:

• high reliability requirements,
• the need to certify the application,
• the ability to operate in an environment having only asynchronous communications.

Given the industrial context, MORSE must provide a methodology and tools to guide the development of the applications mentioned above and make it possible to reach the level of quality required in avionics.

The methodology and tools proposed by MORSE are based on the following five points:

• a prototyping-based approach centered on the concept of model,
• the systematic usage of formal methods,
• automated synthesis of programs from the functional specifications,
• a pivot language to ensure coherence across the different design phases,
• the re-use of existing specifications.

The approach through prototyping is common in industry. The methodology created within the framework of MORSE will be used on this context, and it must therefore be possible to integrate it in a controlled development process. Prototyping is based on the concept of model (stated in a rigorous formalism) that constitutes the clue leading from the specification of a solution to its implementation. However, in the context of distributed applications, this concept has limitations. It is in fact very difficult or even impossible to take into account all possible behaviors of the software  in a prototype since the semantics of such a model is not fully operational.

Formal methods often provide an answer to this problem, justifying their use in MORSE. Their mathematical foundations make it possible to state the expected software properties and to prove them. In the context of a certification process, proofs of properties are a powerful means of helping to achieve compliance with the standard. The formal model will be the starting point for the formal analysis and for the construction of the prototypes. A combination of several techniques is considered: compact representation of all accessible states using Data Decision Diagrams, modular verification, and reduction of the model according to the properties being investigated. In addition, the structural methods made available by a formalism, such as Petri networks, make it possible to verify some properties without calculating the space of states. These two approaches (model checking and structural analysis) will complement each other in MORSE.

Automated program synthesis is the automatic generation of the distributed skeletal code of the application. The code produced like this will allow the rapid construction of prototypes for immediate evaluation of the proposed solution. At the end of the software development cycle, the code generated will be ready for operational deployment on the target platform. MORSE accordingly focuses on generation of the code managing the distribution and the asynchronism, properties that are know to be difficult to implement.

To link the phases of the proposed methodology, MORSE introduces a pivot language. This language will make it possible to use the information of an UML specification. It will also have a formal semantics, to support the analysis of models, and the capabilities of an architecture description language, to link the components of the application. Work centered on LfP (Language for Prototyping), developed at the LIP6, provides a starting point for this pivot language.

A CASE (Computer Aided Software Engineering) prototype will be produced in the context of the MORSE project. It will implement the proposed methodology. It will be used to develop a demonstration application deployed on SAGEM's drone platform.

SAGEM is working with several partners (AONIX, the LIP6, and the LABRI), chosen for their skills and their complementarity in the fields covered by MORSE.

AONIX is a consulting firm and a recognized development environment publisher in the field of critical applications. The company is an active and leading player in the avionics, nuclear, railways transportation, and automotive sectors

The academic partners (the LIP6, the computer lab of Paris VI, and the LABRI (Laboratoire Bordelais de Recherche en Informatique) have done extensive research in formal methods and their applications; both teams have also specialized in the investigation of distributed and asynchronous systems.

The partners form a coherent group whose members have worked together in the past.

Contacts