3rd Workshop on Formal Integrated Development Environment

A satellite workshop of FM2016
General theme of the workshop: “Formal Integrated Development Environment (F-IDE)
for joint construction of an application and its correctness proof upon its formalized specification”.
November 8, 2016, Limassol, Cyprus

News

Aims

High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second one is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third one is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Moreover, tools for testing and static analysis may be embedded in this F-IDE, to help address most steps of the assessment process.

Last year's F-IDE workshop was a satellite event of FM 2015, in June 2015 in Oslo, Norway. The workshop was attended by ~25 participants, and the programme included 10 presentations (7 research papers, and 3 tool demos) and an invited talk given by John Fitzgerald from Newcastle University, UK, on integrated tool chains to support rigorous system design. Post-proceedings have been edited as EPTCS proceedings (EPTCS 187).


Topics

The workshop is opened to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. It should allow the presentation of tools, methods, techniques and experiments. Topics of interest include, but are not limited to, the following:

  • F-IDE building: design and integration of languages, compilation
  • How to make high-level logical and programming concepts palatable to industrial developers
  • Integration of Object-Oriented and modularity features
  • Integration of static analyzers
  • Integration of automatic proof tools, theorem provers and testing tools
  • Documentation tools
  • Impact of tools on certification
  • Experience reports of developing F-IDE
  • Experience reports of using F-IDE
  • Experience reports of formal methods-based assessments of industrial applications

Preliminary Program

9:00-9:05         Welcome

9:05-10:00 Keynote - Kim G. Larsen (Aalborg University, Denmark)

    Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems
    Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. In this talk we will survey how the various component of the UPPAAL tool-suite over a 20 year period has been developed to support various type of analysis of these formalisms. This includes the classical usage of UPPAAL as an efficient model checker of hard real time constraints of timed automata models, but also the branch UPPAAL CORA which have been extensively used to find optimal solutions to time-constrained scheduling problems. More ambitiously, UPPAAL TIGA allows for automatic synthesis of strategies – and subsequent executable control programs – for safety and reachability objectives. Most recently the branch UPPAAL SMC offers a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata, and the branch UPPAAL STRATEGO which supports synthesis (using machine learning) of near-optimal strategies for stochastic priced timed games. The keynote will review the various branches of UPPAAL and highlight their concerted applications to a selection of real-time and cyber-physical examples.

10:00-10:30 Coffee break

10:30-11:00 The KeYmaera X Proof IDE (Stefan Mitsch and André Platzer)

11:00-11:30 Predicting SMT Solver Performance for Software Verification (Andrew Healy, Rosemary Monahan and James Power)

11:30-12:00 Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web (Camille Fayollas, Celia Martinie, Philippe Palanque, Paolo Masci, Michael D. Harrison, Jose C. Campos and Saulo Rodrigues E Silva)

12:00-12:30 The Tinker GUI for graphical proof strategies [tool demo] (Gudmund Grov, Yuhui Lin and Pierre Le Bras)

12:30-14:00 Lunch

14:00-14:30 Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework (Gurvan Le Guernic, Benoit Combemale and José A. Galindo)

14:30-15:00 Extending a user interface prototyping tool with automatic MISRA C code generation (Gioacchino Mauro, Harold Thimbleby, Andrea Domenici and Cinzia Bernardeschi)

15:00-15:30 Extending the Dafny IDE with tactics and dead annotation analysis [tool demo] (Gudmund Grov, Yuhui Lin, Vytautas Tumas, Leon McGregor and Duncan Cameron)

15:30-16:00 Coffee break

16:00-16:30 User Assistance Characteristics of the USE Model Checking Tool [tool demo] (Frank Hilken and Martin Gogolla)

16:30-17:00 Interfacing Automatic Proof Agents in Atelier-B [tool demo] (Lilian Burdy, David Deharbe and Etienne Prun)

17:00-17:15 Closing remarks


Proceedings


Important Dates

  • Paper Submission: September 15, 2016
  • Notification: October 3, 2016
  • Camera-ready: October 26, 2016
  • Workshop: November 8, 2016

PC Co-chairs

  • Catherine Dubois, Samovar / ENSIIE, catherine (dot) dubois (at) ensiie (dot) fr
  • Dominique Mery, LORIA / Université de Lorraine, dominique (dot) mery (at) loria (dot) fr
  • Paolo Masci, HASLab/INESC-TEC and Universidade do Minho, paolo (dot) masci (at) inesctec (dot) pt

Program Committee

  • Bernhard Becket, Karlsruhe Institute of Technology
  • Jens Bendisposto, University of Dusseldorf
  • José C. Campos, HASLab/INESC-TEC and Universidade do Minho
  • Paul Curzon, Queen Mary University of London
  • Michalis Famelis, University of British Columbia
  • Camille Fayollas, IRIT/LAAS
  • Carlo A. Furia, Chalmers University of Technology
  • Andrew Gacek, Rockwell Collins, Inc.
  • Temesghen Kashai, NASA Ames/CMU
  • Kenneth Lausdahl, Aarhus University
  • Rustan Leino, Microsoft Research
  • Stefan Mitsch, Carnegie Mellon University
  • Patrick Oladimeji, Swansea University
  • Andrei Paskevich, Université Paris-Sud/LRI
  • François Pessaux, ENSTA ParisTech
  • Marie-Laure Potet, Laboratoire Vérimag
  • Virgile Prevosto, CEA Tech List
  • Steve Reeves, Waikato University
  • Bernhard Rumpe, RWTH Aachen University
  • Carlo Sacerdoti Coen, University of Bologna
  • Enrico Tassi, INRIA
  • Laurent Voisin, Systerel
  • Makarius Wenzel, sketis.net
  • Yi Zhang, CDRH/FDA