SCADE is a development environment for safety critical embedded software used for more than twenty years in various application domains like avionics, nuclear plants, transportation, automotive. Its code generator is qualified for several industrial standards (DO-178C, IEC 61508, EN 50128, IEC 60880 and ISO 26262) to be used in the development of the most safety critical systems.
Scade is historically based on the synchronous language Lustre designed in Grenoble in the VERIMAG laboratory by its two mains authors Paul Caspi and Nicolas Halbwachs. In its early days, SCADE was mainly seen as a graphical notation for this academic language.
In 2008, a major new version was released, based on the language Scade 6 that extended the dataflow point of view offered by Lustre to integrate new constructs inspired by Esterel and SyncCharts in order to allow more control oriented design style. This language is formally specified following the work of Marc Pouzet on the design of Lucid Synchrone, in particular on the static correction of programs. The formalized aspects cover mainly the static semantics i.e. the type systems that define what a correct program is; this correction is based on four type systems: Types (in the most classical sense), Clocks, Initialization analysis and Causality analyses.
As a formal language, Scade is also well suited to apply formal verification on the applications developed with it. Programs are guaranteed to run in finite memory which allows to use state of the art model checking techniques.
The talk will go through this history, giving some insights on the new Scade 6 constructs, its differences with Lustre and on the development of its qualified code generator.
The formal verification of Scade 6 programs will also be illustrated.