Institute of Cybernetics at TUT
Thursday, 27 November 2014, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Dataflow modelling languages such as Simulink and SCADE are the de-facto tools for the specification and development of control algorithms in high integrity and critical embedded systems. The dataflow models are then translated to software either manually or automatically. While the core semantics of dataflow languages is rather simple and well known, practical designs tend to rely on large complex and/or custom block libraries. Often the behaviour of blocks is further tunable by a large number of parameters, which makes their precise specification and verification challenging.
In this work we have applied some software product line (SPL) principles in the design of a specification language and methodology for specifying the structure and semantics of block libraries. We have identified some key properties that must be ensured in well formed specifications wrt. variablility and semantic consistency. These properties have been formalised in the Why3 language. Block library models can be also automatically translated to the Why3 language. The Why3 toolset and SMT solvers can then be used to either verify or reject the specification.
This is joint work with major contribution from Arnaud Dieumegard and Marc Pantel from IRIT, INP Toulouse.