Date and Location

Room Bolsa-1, Vincci Porto hotel
3rd World Congress on Formal Methods
October 11th, 2019
Porto, Portugal


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.


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 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:
  1. 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
  2. Relational logic (10h30 - 11h30)
    • Modeling with signatures and relations
    • Relational logic operators
    • Exercises: Social Network (1-2)
    • Slides
  3. Analysis (11h30 - 12h30)
  4. 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
  5. 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
  6. Alloy4Fun (17h00 - 18h00)