Model-based Specification

The model-based approach to software specification is arguably the most popular style of formal software specification going today, both VDM and Z being based on this style [Hayes, Jones • Nicholis]. A model-based specification provides a model of a system's state in terms of a collection of state variables. Each state variable models some aspect of the system's retained data as a mathematical object; Z for example uses sets, relations, functions and sequences. System operations are then described in terms of how they modify this state model: pre-conditions define valid inputs and start states for an operation; post-conditions define outputs and the state of the system after operation invocation. State invariants define properties, or constraints, of the system state which must always hold and which operations ate obliged to preserve.

Cited from:
A comparison of the model-based & algebraic styles of specification as a basis for test specification
Source ACM SIGSOFT Software Engineering Notes archive
Volume 21 , Issue 5 (September 1996) table of contents
Pages: 60 - 64
Year of Publication: 1996
ISSN:0163-5948
Author Richard Denney Landmark Graphics Corp.Austin,TX
Publisher
ACM New York, NY, USA