Invited Speakers

Ana Cavalcanti (University of York, UK)
http://www-users.cs.york.ac.uk/~alcc/

Title: From Stateflow Diagrams to Ada via Circus

Abstract: Control engineers make extensive use of diagrammatic notations; control law diagrams are used in industry every day. Techniques and tools for analysis of these diagrams or their models are plentiful; verifcation of code created to implement them, however, is a challenge that has been taken up by few. We have already presented a technique to verify Ada implementations of discrete-time Simulink diagrams; we now extend this work to include stateflow diagrams, which are also part of the Simulink notation. In the avionics and automotive sectors, at least, the use of Simulink to draw and simulate diagrams is standard. Our work is based on industrial tools that produce partial Z and CSP models of diagrams, and on Circus, a notation that combines Z, CSP, and a refnement calculus. By using a combined notation, we provide a specifcation that considers both functional and behavioural aspects of a larger set of diagrams, and support verifcation of a larger number of implementations. We can handle, for instance, arbitrarily large data types and dynamic scheduling

David Deharbe (UFRN, BR)
http://www.consiste.dimap.ufrn.br/~david/

Title: Applying the B Method to Take on the Grand Challenge of Verified Compilation.

Abstract: The B method is a sound and rigorous software engineering process to develop algorithmic implementations from abstract functional specification. This talk shows that the scope of the B method may be extend to encompass, still in a strictly rigorous fashion, a level of detail equivalent to that of assembly languages. We claim and justify that this extension provides for a more reliable software development process as it bypasses two of the less trustable steps in the application of the B method: code synthesis and compilation. The results presented have a value as a proof of concept and may be used as a basis to establish an agenda for the development of an approach to build provably correct compilers based onthe B metho, thus addressing Tony Hoare's grand challenge "The Verifying Compiler" and aspects of Brazilian Computer Society's research challenge nº5.

Patrice Godefroid (Microsoft Research, Redmond, US)
http://research.microsoft.com/users/pg/

Title: Automatic Code-Driven Test Generation

Abstract: Given a program, say with a million lines of C code, wouldn't it be nice to have a tool that could automatically generate a set of input values that would exercize, say, even only 50% or 70% of the code in that program? Today, such a tool does not exist. However, significant progress towards that goal has recently been made. This new line of research combines program analysis, testing, model checking and theorem proving in a novel way. I will describe these latest developments, with a specific emphasis on current work under way at Microsoft. For instance, using a recent prototype tool for automatic code-driven test generation, we have already been able to detect tens of new expensive security-critical bugs in various Microsoft products.

Thierry Jéron (IRISA / INRIA, FR)
http://www.irisa.fr/prive/jeron/

Title: "Symbolic model-based test selection".

Abstract: The talk addresses the problem of off-line selection of test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. Efficient solutions to this problem have been proposed in the context of finite-state models, based on the ioco conformance testing theory. In this talk, we extend this for infinite-state specifications, modelled as automata extended with variables. When considering the selection of test cases according to test purposes (abstract scenarii focused by test cases), the selection of test cases relies on approximate co-reachability analyses using abstract interpretation and syntactical transformations guided by this analysis, while test execution uses constraint solving.