Formal Software Design with Alloy 6

This book is an introduction to formal software specification and analysis with Alloy 6. In this (latest) version, Alloy already allows the specification of behavioural designs with mutable relations and temporal logic, an extension previously implemented in Electrum.

Warning

This version of the book is outdated. The book was extended with a lot of new material and renamed Practical Alloy: A hands-on guide to formal software design. You can find the new version here.

Contents

• An overview of Alloy
  • Specifying a software design
  • Validating a design specification
  • Verifying expected properties
• Structural design with Alloy
  • Signature declaration
  • Field declaration
  • Theme customisation
  • Property specification
  • Assertion verification
  • Using higher-arity relations
  • Exercises
• Protocol design with Alloy
  • Specifying the network configuration
  • Using modules to structure a specification
  • Specifying the protocol dynamics
  • Verifying the expected properties of the protocol
  • Making the specification more abstract
  • Exercises
• Alloy modelling tips
  • Improved visualisation with derived relations
  • An idiom to depict events
  • Using the evaluator to debug specifications
  • Defining test scenarios with formulas
• A relational logic primer
  • Everything is a relation
  • First-order logic in a nutshell
  • Relational operators
  • A type-system for relational specifications
• A temporal logic primer
• Acknowledgements
• Bibliography