KEYNOTE: Jean-Louis Colaço
Ansys
Making tools to support the development of safety-critical embedded software
Abstract: Safety critical systems are systems whose failure may result in loss of human life. The software they embed is just as critical as any of their physical components. Industrial standards provide a framework for developing this software and for certifying the overall system. They include an independent verification that the framework has been respected. Creating tools to support system and software designers in this difficult and costly task is a good place to introduce well-founded technologies, i.e., those based on well-defined programming/modeling languages with strong static properties.
This talk presents, in the context of the DO-178C standard for avionics software development, the fundamentals underlying the SCADE tool suite from Ansys. It focuses on the underlying language and the associated tools for code generation, model coverage, and formal verification by model checking. Particular attention will be given to the coverage of Scade models due to its importance for the objectives defined in DO-178C. Although the latest version of this standard considers formal approaches, model checking is still little used in the certification process. We will identify what is missing to possibly improve this situation.
The talk will conclude with a few important topics for the coming years and a first peek at the next generation of the Ansys tool suite for embedded software: Scade One.
Bio: Jean-Louis Colaço is a Distinguished Engineer at Ansys and works on SCADE Core technologies: the language, compiler and other semantic-based tools. He received his Engineering and Masters degree in 1994 and his Ph.D. in Computer Science from the National Polytechnic Institute of Toulouse in 1997. He started working on the Scade language and its qualified compiler in 1999 and he’s one of the main designers of the Scade 6 language. From 2008 to 2013 he worked at Prover-Technology on certified formal verification doing both tool development and consulting on applications of model checking to railway systems. In 2013 he joined Ansys to continue his work on Scade and now on the Swan language for the next generation of design tools for critical embedded software.
