206
11 avril 2017 - 11h00
Compositional Design and Analysis of Embedded Systems
par Iulia Dragomir de Verimag
11 avril 2017 - 11h00
Compositional Design and Analysis of Embedded Systems
par Iulia Dragomir de Verimag
Abstract: The development of error-free safety critical systems is a challenging task. Several key factors need to be considered: (1) what is the best method for designing large and complex systems with minimal effort and costs, (2) how to guarantee that the designed system is correct with respect to its requirements and (3) how to adapt any theoretical solution to the industrial practice of system design with high-level modeling languages such as Simulink. In this talk we will answer these questions in the context of UML/SysML and Simulink by proposing contract-based compositional reasoning frameworks. A contract models the abstract behavior a component exhibits (i.e., guarantee) in a given context (i.e., assumption). Contract-based reasoning allows to compositionally derive correct components from global system requirements by interposing abstract and partial specifications for components, but also to perform compositional verification of requirement satisfaction.
In the first part we briefly discuss a contract-based framework for UML/SysML designs, where components are formalized as Timed Input/Output Automata and which is instantiated for the OMEGA-IFx toolset.
In the second part we present the Refinement Calculus of Reactive Systems (http://rcrs.cs.aalto.fi), a compositional reasoning framework for Simulink. This framework, implemented in the Isabelle theorem prover, formalizes components as predicate transformers composed in series, parallel and feedback, and allows for compatibility, type and substitutability checking as well as simulation.
