Jean-Louis Colaço ANSYS slides (pdf)

Marie-Claude Gaudel LRI, France slides (pdf)

Patrice Godefroid Microsoft Research, USA

Jean-Louis Colaço

Jean-Louis Colaço is R&D Principal Engineer at ANSYS and works on SCADE Core technologies (language, compiler and other semantic based tools). He received his Engineering and Master 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 with Bruno Pagano and Marc Pouzet with the collaboration of Gérard Berry. 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.

Abstract:

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 software 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.

Marie-Claude Gaudel

Marie-Claude Gaudel is an Emeritus Professor at the University of Paris-Sud at Orsay since 2007.
She was appointed as a professor at this university in 1984. Before joining UPS, she was a researcher at INRIA from 1973 to 1981, and then in charge of the Software Engineering group at the industrial research centre of Alcatel-Alsthom (Marcoussis, France) from September 1981 to January 84.
Her most recognised research achievements are in the area of software testing based on formal specifications, but she has also contributed to other challenging issues such as random software testing and approximate model-checking.
She got the CNRS Silver Medal in 1996 for her work on software testing. She is a Doctor Honoris Causa of EPFL (Lausanne, Switzerland), and of the University of York (UK) where she is an Honorary Visiting Professor since 2015.  She currently holds a Pesquisador Visitante Especial grant of the Ciência sem Fronteiras program with the ICMC centre of the University of São Paulo at São Carlos (Brazil).
In 2011, she has been awarded Chevalier de la Légion d’Honneur. 

Abstract:

Deriving test cases from specifications is now recognized as a major application of formal methods. This paper presents a theory of software testing based on formal specifications and points out the benefits and issues of the use of normal methods to this end.

A notion of exhaustive test set is settled according to the semantics of the formal notation, the considered conformance relation, and some testability hypotheses on the system under test. This gives a framework for the formalization of test selection, test execution, and oracles, and the explicitation of the associated underlying hypotheses on the system under test, such as uniformity hypotheses or regularity hypotheses. This explicitation provides some guide to complementary proofs or tests or instrumentations.

This approach has been illustrated by its application to various formalisms: axiomatic specifications of data types, model-based specifications, process algebras, transition systems, etc. It is at the origin of the development of several test generation environments based on SMT solvers or theorem provers.

Patrice Godefroid

             Patrice Godefroid is a Principal Researcher at Microsoft Research. He received a B.S. degree in Electrical Engineering (Computer Science elective) and a Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at AT&T/Lucent Bell Laboratories, where he was promoted to “distinguished member of technical staff” in 2001. His research interests include program specification, analysis, testing and verification. Patrice is probably best known for his early work on partial-order reduction for model checking concurrent systems (his PhD thesis is published as LNCS volume 1032 by Springer), for his work on VeriSoft, the first software model checker for mainstream programming languages such as C and C++, for his work on 3-valued model checking with may/must abstractions for sound program verification and falsification, and for his work on automatic test generation with DART. More recently, he co-developed SAGE, the first whitebox fuzzer for security testing, which was credited to have found roughly one third of all the security vulnerabilities discovered by file fuzzing during the development of Microsoft’s Windows 7. In 2015, he co-founded Project Springfield, the first commercial cloud fuzzing service. 

Abstract:

Test generation is today the largest application of SMT solvers as measured by computational usage. At Microsoft, the Z3 SMT solver has solved billions of constraints over the last eight years as a component of the whitebox fuzzer SAGE. Whitebox fuzzing extends dynamic test generation based on symbolic execution and constraint solving from unit testing to whole-application security testing. Since 2009, SAGE has been used on a large scale inside Microsoft to automatically ``fuzz'' hundreds of applications. In the process, SAGE found many new security vulnerabilities (missed by blackbox fuzzing and static program analysis) and was credited to have found roughly one third of all the bugs discovered by file fuzzing during the development of Microsoft's Windows 7, saving millions of dollars by avoiding expensive security patches to nearly a billion PCs. In 2015, Project Springfield, now re-named Microsoft Security Risk Detection, became the first commercial cloud fuzzing service, and SAGE also runs in every Springfield fuzzing job. This talk will review these results, and discuss the theory and practice of test generation at an industrial scale.