Tools for creating valid system designs and implementations

By "valid system designs and implemetations", we mean designs and systems that satisfy their requirements. The tools creating such systems can be classified into the following categories:

Suggested tools


CPN - a tool for modeling with Colored Petri Nets (see also Petri Nets World)

LTSA - Labelled Transition System Analyser (see overview of LTSA)

Alloy - a tool based on first-order logic using an object-oriented syntax - for describing and analysing the structure and the behavior of systems

UPPAAL - a tool for modeling extended state machine models possibly including hard real-time constraints (Timed Automata) - have look at the demos that come with the tool.

Other specification methods and tools

UML State Machines -  see here

First-order logic - theorem prover for Z (not suggested for a project)

IOAutomata (for applications of the controller derivation algorithm - not covered in this course in 2013)

Requirements capture tool for Live Sequence Charts (LSC)

Deriving MSCs (or UML sequence diagrams) from User Case Maps

Created: November 6, 2014