Date and Location
Room Bolsa-1, Vincci Porto hotel
3rd World Congress on Formal Methods
October 11th, 2019
Porto, Portugal
Abstract
Good software design is a key to achieve a high-quality system that satisfies all the expected requirements. Having a clear specification of the structures and behaviors of a software system is essential for establishing a trustworthy design, prior to its realisation in actual code. Although a variety of methodologies and frameworks have been proposed to aid the software developer in this crucial task, the most successful ones typically combine a simple yet formal specification language, with automatic analysis tools that allow the user to quickly explore different design alternatives and verify assumptions.
Alloy is a prime example of such a formal method for software design. In Alloy, relational logic is used to describe both a structural design and its desired properties. Relational logic enriches first-order logic with relational algebra operators and closures, enabling a terse but still easily readable style of specification. Following the small scope hypothesis, which states that most bugs can be found with small counter-examples, the Alloy Analyzer verifies properties by checking all cases up to a given user-specified scope. This verification relies on off-the-shelf SAT solvers, and is complemented with techniques to simplify design exploration, namely a customizable graphic visualizer and a symmetry breaking mechanism that eliminates isomorphic structures when iterating over instances or counter-examples.
Alloy has no built-in notion of time or dynamic behavior. Behavior can still be specified and analysed with particular idioms, but this can be rather cumbersome and error prone. Electrum, an extension of Alloy with mutable structures and temporal logic, was recently proposed precisely to simplify this task. Similar to Alloy, in Electrum both the system behavior and its desired dynamic properties are specified declaratively using the same temporal relational logic, a language that adds linear temporal logic operators, including past ones, to relational logic. The Electrum Analyzer shares most of the features of its Alloy counterpart, adding bounded and complete model checking engines to enable the verification of temporal properties.
The goal of this full day tutorial is precisely to introduce participants to Alloy and Electrum, covering a range of topics, from the basics of the logic to more advanced tips on how to tackle larger case studies, including how to debug or improve visualizations to ease the exploration of a design. After the tutorial, participants will be able to develop and analyze simple Alloy and Electrum specifications, and to determine whether these formal methods are well suited to apply in a concrete problem domain (either in a research or industrial context). Educators will also gain access to a sample of materials and examples that could be used to teach Alloy (and Electrum) in their courses.
Prerequisites
No prior knowledge of Alloy or Electrum is required to attend this tutorial, only some basic knowledge of first-order logic and set theory.
Agenda
This full day tutorial will be organised in six sessions, each addressing a particular topic in an interactive format, namely including small exercises and challenges to be solved by the participants. Please download and install the Electrum Analyzer 2.0 here. The tutorial is scheduled for room Bolsa-1 at the Vincci Porto hotel, and agenda is the following:
- Overview (9h00 - 10h00)
- Introduction to formal software design with Alloy and Electrum
- Overview of the specification and analysis techniques with a toy example
- Demo of the Analyzer
- Exercises: Trash (1-3)
- Slides
- Relational logic (10h30 - 11h30)
- Modeling with signatures and relations
- Relational logic operators
- Exercises: Social Network (1-2)
- Slides
- Analysis (11h30 - 12h30)
- Temporal logic (14h00 - 15h30)
- The semantics of mutable signatures and relations
- Linear temporal logic
- Safety and liveness properties
- Fairness constraints
- Model checking with Electrum
- Exercises: Trash (4) and Leader Election (1-4)
- Slides
- Methodology and tips (16h00 - 17h00)
- Tips for developing large case studies, exemplified with the Hybrid ERTMS
- Techniques for better visualisation and scenario exploration
- Exercises and specification challenges with Alloy4Fun
- Exercises: Leader Election (6)
- Slides
- Alloy4Fun (17h00 - 18h00)
Tutors
- Julien Brunel is a Computer Science Researcher at the System & Information Processing Department (DTIS) of the French Aerospace Research Center (ONERA) and at University of Toulouse. He has been working on formal methods, including Alloy and temporal logics, and is one of the proponents of the Electrum language.
- David Chemouil is a Computer Science Researcher at the Systems & Information Processing Department (DTIS) of the French Aerospace Research Center (ONERA), and at Université de Toulouse. He has been researching Alloy-related topics for a decade and is one of the proponents of the Electrum language. He also taught Alloy during several years, as part of a graduate course on formal methods, at ISAE/SupAéro, a French aerospace engineering school.
- Alcino Cunha is an Assistant Professor at Universidade do Minho and researcher at the High-Assurance Software Laboratory of INESC TEC, Portugal. He teaches Alloy at the graduate level since 2007, actively researches on Alloy related topics, and was one of the proponents of the Electrum language.
- Eunsuk Kang is an Assistant Professor of Computer Science in the Institute of Software Research, School of Computer Science at Carnegie Mellon University (CMU), USA. He teaches Alloy as part of a graduate course on software modeling and analysis at CMU. As a previous member of the Alloy team at MIT, he has contributed to the development of the language and the analysis tool, including Alloy*, an extension of Alloy to an analysis of higher-order logics.
- Nuno Macedo is a Computer Science Researcher at the High-Assurance Software Laboratory of INESC TEC, Portugal. He researches on Alloy-related topics and was one of the proponents of the Electrum language. He has also taught Alloy at the graduate level at the University of Minho, Portugal.