Z — ISO/IEC 13568:2002
The standard defines the syntax, type system, and semantics of Z notation. ISO records the edition as current after its review and confirmation in September 2026.
ISO/IEC 13568:2002 (ISO)Formal Description Techniques
Formal specification languages
Formal specifications describe system states or behaviour using a defined syntax and semantics. They make assumptions explicit and allow models to be analysed, tested, or checked against stated properties.
What formal specification can do
Formal description techniques (FDTs) provide mathematical notations for describing systems precisely. Different languages emphasize different views: Z is a state-based notation, while LOTOS and E-LOTOS describe the behaviour of concurrent and distributed systems. VDM is a model-based method with executable specifications and tool-supported analysis.
A formal model can expose ambiguity, inconsistency, or violations of properties within the scope of the model and analysis. It does not automatically prove that an implementation is correct: the model, assumptions, properties, and links to implementation all matter.
International standards
Z, LOTOS, and E-LOTOS
LOTOS — ISO 8807:1989
A formal description technique for the behaviour of distributed and concurrent systems. ISO records the standard as current after its review and confirmation in 2019.
ISO 8807:1989 (ISO)E-LOTOS — ISO/IEC 15437:2001
An enhanced LOTOS language for describing behavioural aspects of distributed and concurrent systems. ISO records the standard as current after its review and confirmation in 2008.
“Current” describes the status of an ISO publication, not how widely a language is used or whether it is the best choice for a new project. Check ISO for later status changes.
Learn and explore
Tools, guides, and background
VDM and Overture
The Overture community maintains language manuals, user guides, tutorials for VDM-SL, VDM++, and VDM-RT, and examples. Its resources also describe using VDM in a development process.
Formal methods resources from Japan
IPA’s practitioner materials include introductory guidance, modelling exercises, and case studies. This is an archive of a programme that ended in 2013; the materials remain available for reference.
Research archive
RLOTOS research on this site
The following papers describe earlier work on extending LOTOS with reflection and using RLOTOS to describe software processes. They are historical research records rather than current introductions to the state of formal methods.
Links and standard status checked on 21 October 2026. Refer to the standards bodies and tool communities for the latest versions.