Date and Location

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 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:
  1. Relational logic
  2. Structural modelling with Alloy
  3. Dynamic modelling with Electrum
  4. Case studies and applications

Tutors