Preface

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. 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. The workshop is a forum of exchange on different features related to F-IDEs.

We solicited several kinds of contributions: research papers providing new concepts and results, position papers and research perspectives, experience reports, tool presentations. The current edition is a one-day workshop where seven communications are given, offering a large variety of approaches, techniques and tools. Each submission was reviewed by three reviewers. The program of this workshop also contains a demo session where three F-IDEs are demonstrated. We have the honor to welcome Professor John Fitzgerald from Newcastle University and he will give a keynote entitled Engineering without Borders: Formal Methods for Systems Design Demand Multidisciplinary Toolchains.

The program committee of F-IDE 2015 was composed of:

Bernhard Beckert, Karlsruhe Institute of Technology
José Campos, Universidade do Minho
Paul Curzon, Queen Mary University of London
Carlo Alberto Furia, ETH Zurich
Thérèse Hardin, UPMC
Rustan Leino, Microsoft Research
Michael Leuschel, University of Düsseldorf
Claude Marché, INRIA
Stefan Mitsch, Carnegie Mellon University
Patrick Oladimeji, Swansea University
Suzette Person, NASA Langley Research Center
François Pessaux, ENSTA ParisTech
Marie-Laure Potet, Laboratoire Verimag
Steve Reeves, Waikato University
John Rushby, SRI International
René Thiemann, University of Innsbruck
Boris Yakobowski, CEA LIST.

We would like to thank the PC members for doing such a great job in writing high-quality reviews and participating in the electronic PC discussion.

We would like to thank all authors who submitted their work to F-IDE 2015. We are grateful to the FM Organisation Committee, which has accepted to host our workshop. The logistics of our job as Program Chairs were facilitated by the EasyChair system and we thank the editors of Electronic Proceedings in Theoretical Computer Science who accepted to publish the papers.

Engineering without Borders: Formal Methods for Systems Design Demand Multidisciplinary Toolchains

This is a great time for formal methods. As computing and networking technology evolves, there are opportunities for software to enhance many physical, social and business systems. Formal methods have the opportunity to give developers new and cost-effective ways of managing the risks of demanding and necessarily multidisciplinary product development but to do so we must target systems, not software alone. In this talk, we will review the recent history of the development of tools to support model-based engineering in VDM, and the ways in which they have evolved towards this vision of real industrial and collaborative use. We highlight the need not just for better tools, but for better integrated toolchains.

Demo Session

Verification-Driven Engineering with Sphinx and KeYmaera X
Stefan Mitsch (Carnegie Mellon University & Johannes Kepler University)

Abstract.
This demo showcases the verification-driven engineering toolset Sphinx [1] and the hybrid system theorem prover KeYmaera X [2].

Sphinx combines model-driven development with formal verification. The goal is to ultimately enable domain experts to interact with verification experts through common models and traceable verification results. Sphinx focuses on modeling tools for hybrid systems, linking these models to formal verification tools, and exchanging models and full or partial proofs. Sphinx is based on the Eclipse platform to integrate graphical and textual modeling, as well as runtime verification techniques [3], refactoring [4], and code synthesis. The modeling features of Sphinx are demonstrated in case studies on autonomous ground robots [5] and road traffic management [6], which are both available for download.

For formal verification we use the verification tool KeYmaera X. KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic and provides a high degree of control over automated proof search. KeYmaera X features a minimal core that isolates soundness-critical axiomatic reasoning. Tactics built on top of this core drive automated proof search, and a modern web-based front-end provides a clean interface for both interactive and automated proving. A tutorial [7] demonstrates how to systematically model, validate, and verify hybrid systems with KeYmaera.

References.
[1] S. Mitsch, G. O. Passmore, A. Platzer. Collaborative Verification-Driven Enginnering of Hybrid Systems. J. Mathematics in Computer Science. Springer, 8(1):71-97, 2014. http://www.cs.cmu.edu/~smitsch/sphinx.html
[2] N. Fulton, S. Mitsch, J.-D. Quesel, M. Völp, A. Platzer. KeYmaera X - An Axiomatic Tactical Theorem Prover for Hybrid Systems. CADE 2015. http://keymaerax.org
[3] S. Mitsch, A. Platzer. ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. RV 2014.
[4] S. Mitsch, J.-D. Quesel, A. Platzer. Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems. FM 2014.
[5] S. Mitsch, K. Ghorbal, A. Platzer. On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. RSS 2013.
[6] S. Mitsch, S. Loos, A. Platzer. Towards Formal Verification of Freeway Traffic Control. ICCPS 2012.
[7] J.-D. Quesel, S. Mitsch, S. Loos, N. Arechiga, A. Platzer. How to model and prove hybrid systems with KeYmaera: A tutorial on safety. STTT, Springer, 2015.

Integrated analysis framework for models and code
Temesghen Kahsai (Carnegie Mellon Silicon Valley/NASA Ames, USA)

Abstract.
Model-based design is widely used in the development of critical control software for embedded systems. Using models is a key to keep the development costs manageable, since correcting bugs on models is much cheaper than on the final implementation. This paradigm can however be effective only when it is accompanied by powerful tools for simulation, verification, synthesis and code generation. The design of embedded control software can be assisted by a variety of modeling languages and tools, among which synchronous languages has become a de-facto standard. Specifically, Simulink [1] has long been used as the standard modeling language of embedded systems. Often Simulink models can call external C functions [2]. For verification, this means that the tools need to reason not only about the Simulink blocks but also about the C functions.

This demo showcases a work in progress of an integrated toolset for the analysis of Simulink models, in which properties are encoded as synchronous observers. The latter, is an extensively used technique to define expected behavior of systems. The toolset consists of (i) sim2lus: a modular compiler from Simulink to Lustre [3], (ii) Zustre [4]: an SMT-based model checker for Lustre code and (ii) SeaHorn [5] a verification tool for LLVM-based languages. The toolset is integrated in the MatLab tool environment, which allows to report directly the outcome of the analysis performed by Zustre and SeaHorn*.

*Currently, only the outcome of Zustre is reported back to MatLab.

References.
[1] www.mathworks.com.
[2] http://www.mathworks.com/help/simulink/ug/incorporate-c-code-using-a-matlab-function-block.html.
[3] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre: A declarative language for programming synchronous systems. In POPL, pages 178-188, 1987.
[4] P-L. Garoche, T. Kahsai, A. Gurfinkel. Syntesizing Modular Invariants for Synchronous Code. In HCVS 2014: 19-30.
[5] http://seahorn.github.io.

Automatic generation of interactive prototypes from formal models using PVSio-web
Paolo Masci (Queen Mary University of London)

Abstract.
PVSio-web is a graphical environment for facilitating the design and evaluation of interactive (human-computer) systems. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analyzing commercial, safety-critical medical devices. It has been used to create training material for device developers and device users. It has also been used for medical device design, by both formal methods experts and non-technical end users. This demo, I will present the latest release of PVSio-web, which will be part of the next PVS distribution. Concrete examples based on commercial medical devices will be used to show the tool functionalities and discuss the rationale behind its design choices. The tool can be freely downloaded from www.pvsioweb.org.

References.
- Tool papers
[1] P. Masci, P. Oladimeji, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby. PVSio-web 2.0: Joining PVS to HCI. To appear in CAV 2015, 27th International Conference on Computer Aided Verification. California, USA, 2015.
[2] P. Oladimeji, P. Masci, P. Curzon and H. Thimbleby. PVSio-web: a tool for rapid prototyping device user interfaces in PVS. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). London, UK, 2013
- Applications
[3] P. Masci, L.D. Couto, P.G. Larsen, P. Curzon. Integrating the PVSio-web modelling and prototyping environment with Overture. In 13th Overture Workshop, co-located with FM2015, Oslo, Norway, 2015
[4] P. Masci, P. Mallozzi, F.L. De Angelis, G. Di Marzo Serugendo, P. Curzon. Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments. In Verisure2015, Workshop on Verification and Assurance, co-located with CAV2015, San Francisco, California, USA, 2015
[5] P. Masci, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby. Formal Verification of Medical Device User Interfaces Using PVS. In ETAPS/FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering, Grenoble, France, 2014
[6] P. Masci, P. Oladimeji, P. Curzon and H. Thimbleby. Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces. In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014). Washington DC, USA, 2014