Working Group on Formal Methods for Industrial Critical Systems

12th International Workshop on Formal Methods for Industrial Critical Systems 

(FMICS 2007)

July 1-2, 2007,

Berlin, Germany

Affiliated with CAV 2007 conference

Registration is possible via CAV using this link

Programme

Sunday, July 1

8:45 – 9:00 Welcome

9:00 – 10:00 Invited Talk

Charles Pecheur (Catholic University of Louvain)

Verification of Embedded Software: from Mars to Actions

10:00 – 10:30  Coffee Break

10:30 – 12:00 Session 1:  Control Systems

Sylvie Putot, Eric Goubault, Philippe Baufreton and Jean Gassino

Static Analysis of the Accuracy in Control Systems: Principles and Experiments

Bastian Schlich, Jann Löll and Stefan Kowalewski,

Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code

Sören Preibusch and Florian Kammüller

Checking the TWIN Elevator System by translating Object-Z to SMV           

12:00 – 14:00 Lunch

14:00 – 15:30 Session 2:  Scheduling  and Time I

Kirsten Winter, Paul Strooper and Lionel van den Berg

Introducing Time in an Industrial Application of Model Checking

Michael Whalen, Darren Cofer, Steven Miller, Bruce Krogh, Walter Storm

Integration of Formal Analysis into a Model-Based Software Development Process

Lars Gesellensetter, Sabine Glesner and Elke Salecker 

Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler

15:30 – 16:00 Coffee Break

16:00 – 17:00 Session 3: Scheduling  and Time II

Murali Rangarajan and Darren Cofer

Computing Worst-case Response Times in Real-time Avionics Applications

Leonard Lensink, Sjaak Smetsers and Marko van Eekelen,

Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization 

20:00 Workshop Dinner

Restarurant Mutter Hoppe (Rathausstr. 21)

Monday, July 2

9:00 – 11:00 Invited Talks shared with ARTIST

Thomas Henzinger (EPFL Lausanne)

The Embedded Systems Design Challenge

Gérard Berry (Esterel Technologies)

Synchronous Design and Verification of Critical Embedded Systems using SCADE and Esterel

11:00 – 11:30  Coffee Break

11:30 – 12:30 Session 4: Verification

Maurice ter Beek, Alessandro Fantechi, Stefania Gnesi and Franco Mazzanti 

An Action/state-based model-checking Approach for the Analysis of an Asynchronous Protocol for Service-Oriented Applications

Radek Pelanek

Model Classifications and Automated Verification       

12:30 – 14:00 Lunch

14:00 – 15:30 Session 5: Software

Robert Palmer, Ganesh Gopalakrishnan, Robert Kirby and DeLisi, Michael

An Approach to Formalization and Analysis of Message Passing Libraries

Marko van Eekelen, Stefan ten Hoedt, René Schreurs and  Yaroslav S. Usenko

Analysis of a Session-Layer Protocol in mCRL2. Verification of a Real-Life Industrial Implementation

Santiago Escobar, Maria Alpuente and Mauricio Alba-Castro, 

Automatic Certification of Java Source Code in Rewriting Logic         

15:30 – 16:00 Coffee Break

16:00 – 17:00 Session 6: Testing

Ana Paiva, João Pascoal Faria and Pedro Mendes

 Reverse Engineered Formal Models for GUI Testing

Alexandra Desmoulin and Cesar Viho

Automatic Interoperability Test Case Generation based on Formal Definitions

17:00 Closing

Invited talks

1. Charles Pecheur (Catholic University of Louvain, Belgium): Verification of Embedded Software: from Mars to Actions

Abstract:

Embedded controllers are more and more pervasive and feature more and more advanced capabilities. For space applications in particular, the development of autonomous controllers is seen as a critical technology to enable new mission objectives and scale down operating costs. On the flip side, the validation of intelligent control software poses a huge challenge, both due to the increased complexity of the system itself and the broad spectrum of normal and abnormal conditions in which it has to be able to operate. This talk will follow our journey in applying some modern, analytical verification technologies and tools to the validation of autonomy software, in the context of space applications, at NASA Ames Research Center in California. This route will take us from the concrete, practical dependability requirements for space-bound software that motivated the work down to the deeper, broader issues in formal methods that emerged as part of that work. Our work has focused on analysing model-based approaches to fault diagnosis, as exemplified by NASA Ames’ Livingstone system. We developed two lines of verification tools for model-based diagnosis applications, and experimented with those tools on real-size problems taken from NASA applications.

Under different angles, both approaches stem from model checking principles. Verifying diagnosis systems and models has led to considering the issue of diagnosability: given a partially observable dynamic system, and a diagnosis system observing its evolution over time, how to verify (at design time) whether the system provides sufficient observations to determine and track (at run-time) its internal state with sufficient accuracy. This kind of question can be reduced to a state reachability problem, which can be solved using (symbolic) model checking. In turn, diagnosability can be phrased as a particular temporal and epistemic property (“the diagnoser always knows the faults”), and we have carried experiments in applying a generic temporal-epistemic model checker to our diagnosis applications. Finally, epistemic models and logics themselves can, under some assumptions, be reduced to labelled transition systems and action-based temporal logics. We implemented this reduction and added support for this logics in NuSMV, thereby leveraging NuSMV’s language, features and ecosystem to the analysis of epistemic (and, more broadly, action-based) properties.

2. Tom Henzinger (EPFL Lausanne): The Embedded Systems Design Challenge (based on a joint position paper with Joseph Sifakis)

Abstract:

We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.

3. Gerard Berry (Esterel Technologies): Synchronous design and verification of critical embedded systems using SCADE and Esterel

Abstract:
SCADE (Safety Critical Application Design Environment) is a design environment dedicated to safety-critical embedded software applications. It is widely used for avionics, railways, heavy industry, and automotive applications. For instance, most critical systems of the Airbus A380 have been developed with SCADE. The core element is the Scade synchronous formalism, which can be viewed as a graphical version of Lustre coupled with synchronous hierarchical state machines. The Scade to C compiler is certifiable at level A of DO-178B avionics norm, which removes the need for unit-testing the embedded C code and brings big savings in the certification process. The SCADE tools encompasses a simulator, a model coverage analyzer, a formal verifier, a display generator, and gateways to numerous other prototyping or software engineering tools. Esterel Studio is a similar hardware modeling, design, and verification environment based on the Esterel v7 formal synchronous language. Esterel Studio is used by major semiconductor companies to specify, verify, and synthesize complex hardware designs.
It can generate both an optimized circuit and a behaviorally equivalent software model from a single formal specification. It also supports simulation and formal verification, which is widely used in production applications. We discuss the advantages and limitations of the underlying synchronous concurrency model. We explain why the same core science and technology can be applied to such different domains, however with quite different integration in global system-level design flows according used in the different industries.

Scope of the workshop

The aim of the FMICS workshop series, which is celebrating its tenth issue, is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops are intended to bring together scientists and practitioners who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications.

Topics include, but are not restricted to:

• Design, specification, code generation and testing with formal methods.
• Verification and validation of complex, distributed, real-time systems and embedded systems.
• Verification and validation methods that aim at circumventing shortcomings of existing methods in respect to their industrial applicability.
• Tools for the design and development of formal descriptions.
• Case studies and project reports on formal methods related projects with industrial participation (e.g. safety critical systems, mobile systems, object-based distributed systems).
• Application of formal methods in standardization and industrial forums.

Previous workshops of the ERCIM working group on Formal Methods for Industrial Critical Systems were held in  Oxford (March 1996),  Cesena (July 1997),  Amsterdam (May 1998),  Trento (July 1999), Berlin (April 2000),  Paris (July 2001),  Malaga (July 2002) , Trondheim (June 2003), Linz (September 2004), Lisbon (September 2005) and Bonn (August 2006).

Important dates

Deadline for abstracts	30 March 2007 7 April 2007
Deadline for papers	7 April 2007 14 April 2007
Accept/Reject Notification	14 May 2007 17 May 2007
Final Manuscript for participants proceedings	31 May 2007 15 June 2007
Workshop	1-2 July 2007
Revised version for LNCS	15 September 2007
Author notification for LNCS	30 September 2007

Organizers

Stefan Leue (University of Konstanz, Germany)

Pedro Merino (University of Malaga, Spain)

Contact: fmics2007-chairs@lcc.uma.es

Programme committee

Per Bjesse (Synopsys, USA)

Lubos Brim (University of Masaryk, Czech Republic)

Marsha Chechik (University of Toronto, Canada)

Darren Cofer (Rockwell Collins, USA)

Stefania Gnesi (ISTI-CNR, Italy)

Patrice Godefroid (Microsoft Research, USA)

Michael Goldsmith (Formal Systems, UK)

David Harel (Weizmann Institute of Science, Israel)

Connie Heitmeyer (Office of Naval Research, USA)

Leszek Holenderski (Philips, Netherlands)

Joost-Pieter Katoen (RWTH Aachen, Germany) 

Roope Kaivola (Intel, USA)

Stefan Kowalewski (RWTH Aachen, Germany)

Salvatore La Torre (Universita' degli Studi di Salerno, Italy)

Martin Leucker (TU München, Germany)

Stefan Leue (University of Konstanz, Germany), Co-Chair

Radu Mateescu (INRIA Rhone-Alpes, France)

Pedro Merino (University of Malaga, Spain), Co-Chair

David Parker (University of Birmingham, UK)

Charles Pecheur (Université Catholique de Louvain, Belgium)

Francois Pilarski (Airbus, France)

Andreas Podelski (University of Freiburg, Germany)

Jakob Rehof (University of Dortmund, Germany)

John Rushby (SRI International, USA)

Don Sannella (University of Edinburgh, UK)

Ina Schieferdecker (Fraunhofer FOKUS, Germany)

Anna Slobodova (Intel, USA)

Jaco van de Pol (CWI, Netherlands)

Farn Wang (National Taiwan University, Taiwan)

Willem Visser (SEVEN Networks, USA)

Submissions

Submissions must be made electronically through the Online Conference Service.

Papers should be up to 16 pages in LNCS format, with the names and affiliations of the authors and a clear and informative abstract. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. All submissions must report on original research Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any such published or concurrently submitted paper must be clearly indicated.

Publication

Workshop proceedings will be available during the workshop. Additional post-workshop proceedings will be published by Springer Verlag in the Lecture Notes in Computer Science series.

Revised versions of selected papers will be invited for a special section of Springer's International Journal on Software Tools for Technology Transfer (STTT).

Best paper award

The European Association of Software Science and Technology is offering an award to the best FMICS paper.

Back to FMICS WG