Methods

The ASM method applies Abstract State Machines (ASMs) to support traceable rigorous design and analysis (by experimental testing and/or mathematical verification) of software-intensive systems. The following three ingredients of the method support to develop executable code from specifications by stepwise refinement where at each step both mathematical verification of desired properties and experimental model validation by testing can be applied and fully documented to permit design for change.

The Alloy language can be used to describe structures based on a collection of constraints. This created Alloy model can then be analyzed by the Alloy Analyzer, a solver that finds concrete structures that satisfy the constraints defined in the Alloy model. The analysis can be used to generate sample structures or to check properties of these structures by trying to generate counterexamples. Alloy is based on the Z specification language and Tarski’s relational calculus.

Classical B (or just B) focuses on a tool-based refinement of a formal specification to code. It is based on the Z notation but slightly more low-level. In B a system consists of an abstract machine in which the modeler specifies the goal of the system. Via several refinement steps, this abstract goal is enhanced by more details on a less abstract level by adding details about data structures and algorithms that define how the goal is achieved. All steps are proven correct until a deterministic version (the implementation) is reached.

TLA+ (Temporal Logic of Actions) was developed by Leslie Lamport to model, document, and verify especially concurrent and distributed systems. The language aims for defining the set of all correct system behaviors. It is organized in modules that contain a definition of states and (conditional) state transitions in form of steps. A “next-state-relations” defines how variables can change in any step. Similar to Z, B, and Event-B TLA+ is based on the Zermelo-Fraenkel set theory, but extended with built-in temporal logic operators.

In the Vienna Development Method (VDM) models consist of a rich representation of data on which a system operates, together with the functionality that should be executed on these data structures. Besides the internal data also external input/output data is considered in the models.

Z is the “ultimate language” as stated by Jean-Raymond Abrial who invented this formal specification language in 1977. This language aims for a precise and clear specification of computer-based systems based on the Zermelo-Fraenkel set theory, lambda calculus, and first-order predicate logic. The main elements of Z are so-called “schemata” that consist of typed variables and constraints on the assignment of these. Z provides a standardized catalogue of often used mathematical functions and predicates.