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.

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.

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.

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.

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.