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.

About the speaker

Jean-Louis Colaço is R&D Distinguished Engineer at ANSYS and works on SCADE Core technologies (language, compiler, and other semantic based tools). He received his Engineering and master’s degree in 1994 and his Ph.D. in Computer Science from the National Polytechnic Institute of Toulouse in 1997. He started working on Scade language in 1999 and his one of the main designers of Scade 6 language. From 2007 to 2008 he worked in the innovation group at Siemens-VDO as a project manager in the powertrain department. From 2008 to 2013 he was at Prover-Technology working on certified formal verification doing both tool development and consulting on application of model checking to railways systems.

Jean-Louis Colaço is R&D Distinguished Engineer at ANSYS and works on ANSYS® SCADE Suite® Core technologies (language, compiler, and other semantic based tools).

He received his Engineering and master’s degree in 1994 and his Ph.D. in Computer Science from the National Polytechnic Institute of Toulouse in 1997.

He started working on Scade language and compilation in 1999 and his one of the main designers of Scade 6 language.

From 2007 to 2008 he worked in the innovation group at Siemens-VDO as a project manager in the powertrain department.

From 2008 to 2013 he was at Prover-Technology working on certified formal verification doing both tool development and consulting on application of model checking to railways systems.