FSA Groep

Welcome to the FSA pages. The group FSA is concerned with the design, description and especially validation and verification of the behaviour of systems.

Using programming languages, compilers and debuggers it is fairly easy to write programs which allow contemporary systems to perform amazing tasks. But the programs grow quickly, generally resulting in overwhelming complexity. From such a point improving the program takes extensive effort and programming becomes a frustrating and expensive affair.

The OAS group directs itself to keep programs under control. The behaviour of systems is described abstractly, for instance using the languagemCRL2. Furthermore, these descriptions are analyzed either by hand, or using computer based tools, in order to show that they are well behaved. The tools are based on a wide range of techniques: labelled transitions systems, term rewriting, binary decision diagrams with equalities, etc.

Examples of applications and developed technology are

IEEE 1394.1 FireWire Net Update Protocol
From 1996 onwards, the IEEE 1394.1 Working Group has worked on the IEEE P1394.1 draft standard for Serial Bus Bridges. As a case study for the IQPS project, the Net Update protocol has been studied extensively. Read on...

Distributed Algorithms
Some of the most intriguing distributed algorithms are wait- and lock-free algorithms. These do not allow synchronization primitives such as semaphores and mutexes. Read on...

Automated Reasoning
Many problems, in particular in the area of verification of computer systems, can be expressed as validity of some big formula. Typical issues include proving this validity automatically, and find a unique representation.

Tools
We contribute to the following tools that are publicly available:

  • mCRL A language and tool set to study communicating processes with data.
  • mCRL2 The successor of mCRL.
  • Heerhugo A propositional theorem prover.
  • Torpa A tool for automatically generating proofs of termination of string rewriting.