Joint Hamilton Institute/Computer Science Department Seminar

Thursday, February 13, 2020 - 13:00 to 14:00
Hamilton Institute Seminar Room (317), 3rd Floor Eolas Building

Speaker: ​Professor Dominique Mery, INRIA, LORIA and Universite de Lorraine, France

Title: "Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661"

Abstract: The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof assistants.  The difficulties, even for powerful tools, lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algorithms.

Verification by construction can be achieved by using  a formal framework in which models are constructed at different levels of abstraction; each level of abstraction is refined by the one below, and this refinement relationships is documented by an abstraction relation  namely a gluing invariant.

The highest levels of abstraction are used to express the required behavior in terms of the problem domain and the lowest level of abstraction corresponds to  an implementation from which an efficient implementation can be derived automatically. In this talk, we describe a methodology based on the general concept of refinement and used for developing distributed algorithms satisfying a given list of safety and liveness properties.

The modelling methodology  is defined in the Event-B modelling language using the IDE Rodin. The case study that we demonstrate is the development of safety critical software for ARINC 661. ARINC 66 is a standard which aims to normalize the definition of a Cockpit Display System (CDS), and the communication between the CDS and User Applications which manage aircraft avionics functions.

Keywords:
Correct-by-Construction, Modelling, Refinement, Distributed Algorithms, Verification, Proof Assistant.