Published: 27th January 2017
DOI: 10.4204/EPTCS.240
ISSN: 2075-2180

EPTCS 240

Proceedings of the Third Workshop on
Formal Integrated Development Environment
Limassol, Cyprus, November 8, 2016

Edited by: Catherine Dubois, Paolo Masci and Dominique Méry

Preface
Catherine Dubois, Paolo Masci and Dominique Méry

Keynote

Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems
Kim G. Larsen

Regular Papers

Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web
Camille Fayollas, Célia Martinie, Philippe Palanque, Paolo Masci, Michael D. Harrison, José C. Campos and Saulo Rodrigues e Silva
1
Predicting SMT Solver Performance for Software Verification
Andrew Healy, Rosemary Monahan and James F. Power
20
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
38
Extending a User Interface Prototyping Tool with Automatic MISRA C Code Generation
Gioacchino Mauro, Harold Thimbleby, Andrea Domenici and Cinzia Bernardeschi
53
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving
Stefan Mitsch and André Platzer
67

Short Papers

Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"
Lilian Burdy, David Déharbe and Étienne Prun
82
User Assistance Characteristics of the USE Model Checking Tool
Frank Hilken and Martin Gogolla
91

Tool Papers

The Tinker GUI for Graphical Proof Strategies (tool demo)
Gudmund Grov, Yuhui Lin and Pierre Le Bras
98
Extending the Dafny IDE with Tactics and Dead Annotation Analysis (tool demo)
Gudmund Grov, Yuhui Lin, Léon McGregor, Vytautas Tumas and Duncan Cameron
102

Preface

F-IDE 2016 is the third Formal Integrated Development Environment workshop (F-IDE 2016) held in Limassol, Cyprus, on November 8, 2016 as a satellite workshop of the FM conference.

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 with eight communications, offering a large variety of approaches, techniques and tools. Some of the presentations took the form of a tool demonstration. Each submission was reviewed by three reviewers.

We had the honor to welcome Professor Kim G. Larsen from Aalborg University. He gave a keynote entitled Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems.

The program committee of F-IDE 2015 was composed of:
Bernhard Becket, Karlsruhe Institute of Technology
Jens Bendisposto, University of Düsseldorf
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 Verimag
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
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 2016. 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.


Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems

Kim G. Larsen (Department of Computer Science, Aalborg University, Denmark)

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 components of the UPPAAL tool-suite over a 20 year period have been developed to support various 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 has 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. More 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 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.


The Tinker GUI for Graphical Proof Strategies (tool demo)

Gudmund Grov (Heriot-Watt University)
Yuhui Lin (Heriot-Watt University)
Pierre Le Bras (Heriot-Watt University)

1 Background

Most interactive theorem provers provide users with a tactic language in which they can encode common proof strategies in order to reduce user interaction. To encode proof strategies, these languages typically provide: a set of functions, called tactics, which reduce sub-goals into smaller and simpler sub-goals; and a set of combinators, called tacticals, which combines tactics in different ways.

Composition in most tacticals either relies on the number and the order of sub-goals, or tries all tactics on all sub-goals. The former is brittle as the number and the order could be changed if any of the sub-tactics changes; and the latter is hard to debug and maintain, as if a proof fails the actual position is hard to find. It is also difficult for others to see the intuition behind tactic design.

2 PSGraph

To overcome these issues we developed PSGraph, a graphical proof strategy language [2], where complex tactics are represented as directed hierarchical graphs. Here, the nodes contain tactics or nested graphs, and are composed by labelled wires. The labels are called goal types: predicates describing expected properties of sub-goals. Each sub-goal becomes a special goal node on the graph, which ``lives'' on a wire. Evaluation is handled by applying a tactic to a goal node that is on one of its input wires. The resulting sub-goals are sent to the out wires of the tactic node. To add a goal node to a wire, the goal type must be satisfied. This mechanism is used to control that goals are sent to the right place, independently of number and order of sub-goals. For more details see [2].

A PSGraph can have the following types of nodes:

Figure 1: A PSGraph example [7]

To illustrate, consider the PSGraph in Figure 1. This example is taken from [7]. It is an encoding of a simple tactic from ProofPower to eliminate quantifiers. The overall strategy (i.e. the top-level graph on the right) contains an atomic tactic that repeatedly strips conjunctions (strip_∧), and two hierarchical nodes: one deals with existentially quantifier variables (simp_ex); the other deals with universal quantifiers (simp_forall). The goal types are used to send the goals to the correct node, and to decide when to terminate the loop.

3 The Tinker Tool

In [3], we introduced the Tinker tool, which implements PSGraph with support for Isabelle/HO [2, 3], ProofPower [3, 6, 7] and Rodin [4]. Within the ProofPower tool, we are also investigating industrial usage of PSGraph and Tinker [6].

A PSGraph in Tinker can be applied as a normal tactic/method within the (Isabelle, ProofPower or Rodin) proof IDE. This is the normal execution. However, if it fails, it can instead be run in an `interactive mode' where the Tinker GUI is used to visualise and guide how the proof proceeds and identify where it failed. Figure 2 shows this GUI.

Figure 2: The Tinker GUI and its layout [7]

A user can draw a PSGraph from the Graph panel by selecting the type of node from the Drawing and evaluation controls panel. Nodes are connected by dragging a line between them. When selecting an entity, the details are displayed in the Information panel, and they can be edited by double clicking. The Drawing and evaluations controls panel gives users a lot of flexibility when developing and applying proof strategies, including:

  1. select which goal to apply;
  2. choose between stepping into and stepping over the evaluation of hierarchical nodes;
  3. apply and complete the current hierarchical tactic;
  4. apply and finish the whole proof strategy;
  5. insert a breakpoint and evaluate a graph automatically until the break point is reached by a goal.
Tinker also provides features to export PSGraphs and record proofs -- [7] for further details.

4 Summary

With the exception of simple proof visualisation (e.g. [5]), we are not familiar with any other graphical proof tools to support theorem provers. While there are tactic languages that support robust tactics (e.g. Ltac [1] for Coq or Eisbach [8] for Isabelle), we believe that the development and debugging features of Tinker are novel. Several features of the tool have been motivated by working with D-RisQ (www.drisq.com) in encoding their highly complex Supertac proof strategy in ProofPower [6].

In the future, we would like to improve static checking of PSGraph; for example that all atomic tactics used in the graph exist. We are also interested in investigating (semi-)automatic translations from traditional tactic language into PSGraph. This will also include more modern tactic languages, such as Ltac and Eisbach. We also plan to improve the layout algorithm, and develop and implement a better framework for combining evaluation and user edits of PSGraphs.

References

  1. D. Delahaye (2002): A Proof Dedicated Meta-Language. Electronic Notes in Theoretical Computer Science 70(2), pp. 96-109. doi:10.1016/S1571-0661(04)80508-5.
  2. G. Grov, A. Kissinger & Y. Lin (2013): A Graphical Language for Proof Strategies. In: LPAR 2013, Springer, pp. 324-339. doi:10.1007/978-3-642-45221-5_23
  3. G. Grov, A. Kissinger & Y. Lin (2014): Tinker, tailor, solver, proof. In: UITP 2014, ENTCS 167, Open Publishing Association, pp. 23-34. doi:10.4204/EPTCS.167.5.
  4. Y. Liang, Y. Lin & G. Grov (2016): 'The Tinker' for Rodin. In: ABZ 2016, Springer, pp. 262-268, doi: 978-3-319-33600-8_19
  5. T Libal, M. Riener & M Rukhaia (2014): Advanced Proof Viewing in ProofTool. In: UITP 2014, EPTCS 167, Open Publishing Association, pp. 35-47. doi: 10.4204/EPTCS.167.6.
  6. Y. Lin, G. Grove, C. O'Halloran & P. G. (2016): A Super Industrial Application of PSGraph. In: ABZ 2016, Volume 9675 of LNCS, pp. 319-325, Springer. doi: 10.1007/978-3-319-33600-8_28.
  7. Y. Lin, P. Le Bras & G. Grov (2016): Developing and Debugging Proof Strategies by Tinkering. In M. Chechik & J.-F. Raskin, editors: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, Berlin, Heidelberg, pp. 573-579, doi: 10.1007/978-3-319-33600-8_28.
  8. D. Matichuk, M. Wenzel & T. Murray (2014): An Isabelle Proof Method Language, In: ITP 2014, Volume 8558 of LNCS, pp. 390-405. Springer International Publishing, Vienna, Austria, doi: 10.1007/978-3-319-08970-6_25.

Extending the Dafny IDE with Tactics and Dead Annotation Analysis (tool demo)

Gudmund Grov (Heriot-Watt University)
Yuhui Lin (Heriot-Watt University)
Léon McGregor (Heriot-Watt University)
Vytautas Tumas (Heriot-Watt University)
Duncan Cameron (Heriot-Watt University)

1  Introduction

Dafny [4] is a verification-aware programming language where the specification of desired properties is intertwined with their implementation in the program text. It uses an automated theorem prover to prove that the specification is satisfied by the program. A specification serves two purposes: (1) it specifies the properties to be proven and acts as a documentation of the program, which is desirable to include in the program text; (2) it is used to guide the prover if a property cannot be verified without help. This is a necessary evil, which is not desirable and may obfuscate the readability of the program text. We will call these specification elements that are only there to guide the prover for proofs.

Dafny has a Visual Studio IDE plug-in [6], which seamlessly applies the verification in the background. In this demonstration we will show two extensions to this IDE:

2  Working with Dafny tactics in the IDE

Tacny is a conservative extension of Dafny with features to implement verification patterns as tactics [1, 2]. This tactic language is a meta-language for Dafny, where evaluation of a tactic works at the Dafny level: it takes a Dafny program with tactics and tactic applications, evaluates the applications and produces a new valid Dafny program, where tactic calls are replaced by Dafny constructs that tactics have generated.

A tactic is a special Dafny ghost method, recognisable by the tactic keyword. It contains many features to talk about a program, and features to generate proofs in terms of Dafny by transforming the program. A crucial property is that neither the program, nor the actual (non-proof) specification, can be changed – which we call contract-preserving transformations [>1]. To illustrate, consider the following tactic:

tactic myTac(v:Element,t:Tactic)
{
tactic match v { t(); }
}
The myTac tactic generalises the notion of pattern matches (A Dafny match statement). As argument it takes a variable v which is assumed to be of an inductively defined datatype. The tactic match statement will then generate a match statement and a case for each constructor of the datatype, and apply tactic t() to each case. A tactic is evaluated by the Dafny verifier and the code generated is hidden from the user. Within a verified method that contains a tactic application, the code generated by the tactic can be made available in two different ways. This is illustrated by the ‘refactoring’ menu available by right-clicking the tactic application:

If the user selects ‘Read-only peek this tactic (F9)’ then a read-only window will appear in the editor, where the code is shown. This will not make any changes to source code:

A second alternative is to ‘Expand this tactic (F10)’. Here, the code that the tactic application generated will replace the tactic call. This is illustrated by the following screenshot:

Finally, in the top-level menu, a user can either disable tactics, meaning all tactic applications will be ignored, or expanding all tactic applications in the program:

The last option is to remove all “dead annotations”, which we discuss next.

3  Dead annotation removal

(This section is an adaptation of [1])

A fully verified Dafny program may contain unnecessary proof annotations, which may obfuscate the program text. There are at least two reasons for why such “dead annotations” may be present:

  1. Proof constructs are normally added incrementally to the program text until a proof is found. Previous increments may not have helped to progress the proof, but are left by the user.
  2. The underlying verifier is improved such that guidance that used to be required is no longer needed.

Inspired by the dead code optimisation< found in most compilers, we have developed a tool called DARe (Dead Annotation Removal) that works by traversing the Dafny abstract syntax tree and remove as many annotations as possible. Each time an annotation is removed, Dafny is applied to check if the program still verifies, and the constructs will only be removed if Dafny does not complain. Here an annotation can be:

We are integrating the DARe tool into the Dafny Visual Studio IDE. It will initially apply DARe to all methods (that does not have any verification errors) after the IDE has remained idle (i.e. no user-interaction) for at least 10 seconds. As DARe will be relatively slow to run, it will terminate (with failure) once a user starts interacting with the system. When it successfully terminates, all unnecessary (or dead) annotations will be highlighted (underlined and greyed out). This is illustrated on line 31 of the following screen-shot:

The user can then press the light-bulb to get the options of removing the given dead annotation or all dead annotations of the method or file, as illustrated below:

The different options will behave as follows:

The tool will keep track of any methods that are changed since last time DARe was applied and will reapply DARe when a method have changed. Again, this will only happen if the method does not have any verification errors and the system remains idle for 10 seconds.

4  Summary

This tool demonstration shows two extensions to the Dafny Visual Studio IDE. Both of the extensions have the ability to improve the program text and to support users when developing Dafny programs: re-usable tactics can replace proofs by high-level proof patterns, while proof elements that are not required can be removed in a semi-automatic manner.

References

  1. Duncan Cameron, Gudmund Grov, and Léon McGregor (2016): What is your actual annotation overhead? In informal proceedings of the 28th Nordic Workshop on Programming Theory (NWPT 2016). Kim G. Larsen and Jiri Srba (editors), pp. 15-17. Available from http://nwpt2016.cs.aau.dk/nwpt2016-proceedings.pdf.
  2. Gudmund Grov, Yuhui Lin, and Vytautas Tumas (2016): Mechanised Verification Patterns for Dafny. In 21st International Conference on Formal Methods (FM 2016), pages 326-343, volume 9995 of LNCS, Springer, doi:10.1007/978-3-319-48989-6_20.
  3. Gudmund Grov and Vytautas Tumas (2016): Tactics for the Dafny Program Verifier. In Marsha Chechik and Jean-François Raskin, editors, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 36-53. Springer, 2016. doi:10.1007/978-3-662-49674-9_3
  4. K. Rustan M. Leino (2010): Dafny: An automatic program verifier for functional correctness. In LPAR 2010, volume 6355 of LNCS, pages 348–370. Springer-Verlag, doi:10.1007/978-3-642-17511-4_20
  5. K. Rustan M. Leino and Nadia Polikarpova (2013): Verified Calculations. In VSTTE, 2013. Volume 8164 of LNCS, pages 170-190. doi:10.1007/978-3-642-54108-7_9
  6. K. Rustan M. Leino and Valentin Wüstholz (2014): The Dafny integrated development environment. In Proceedings F-IDE 2014, EPTCS 149, 2014, pp. 3-15. doi:10.4204/EPTCS.149.2

This work has been supported by EPSRC grants EP/M018407/1 and EP/N014758/1. Special thanks to Rustan Leino and his colleagues at MSR. The work is an adaptation of features presented in [2, 3, 1].