Date and Location3rd World Congress on Formal Methods
October 11th, 2019
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.
AbstractAlloy 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.
No prior knowledge of Alloy or Electrum is required to attend this tutorial, only some basic knowledge of first-order logic and set theory.
This full day tutorial will be organized in four sessions of 1h30m, each addressing a particular topic in an interactive format, namely including small exercises and challenges to be solved by the participants. The four topics that will be addressed are:
- Relational logic
Structural modelling with Alloy
- Introduction to lightweight formal methods
- First order logic
- Relational algebra operators and closures
- Automatic analysis of relational logic
Dynamic modelling with Electrum
- Signature and field declaration, type system
- Modules, predicates, and functions
- Facts, asserts, analysis commands, and scopes
- Introduction to the visualizer, themes, and the evaluator
- The standard util library
Case studies and applications
- Mutable signatures and fields
- Linear temporal relational logic operators
- The event language
- Automatic analysis of temporal relational logic
- Methodology for developing larger specifications
- Tips for improving the visualization for easier model validation
- Debugging models with unsat cores and test scenarios
- Examples: Same-Origin Policy, Hybrid ERTMS, Chord
- 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.