What Are Specification Languages?

Specification languages are formal notations used to describe the intended behavior, structure, or properties of a hardware or software system with mathematical precision. Unlike natural-language requirements, a specification written in a formal language is amenable to automated analysis: tools can check consistency, detect ambiguities, and verify that an implementation satisfies the specification without relying on human review alone. Specification languages draw from mathematical logic, set theory, and automata theory, and they occupy a distinct role in the development process between informal requirements and executable code.

The field traces its origins to the 1960s and 1970s, when researchers sought rigorous alternatives to prose-based system descriptions for safety-critical software. Early milestones include the development of Z notation at the Oxford University Programming Research Group in the late 1970s and the Vienna Development Method (VDM), which originated from IBM's work on formally describing the PL/I programming language. Both approaches grounded specification in typed set theory and first-order predicate logic, providing a framework for proving properties of a design before it was built.

Formal Specification Methods

Formal specification methods use mathematical structures to express what a system must do, independent of how it is implemented. Z and VDM specify system state as typed sets and define operations as predicates that constrain the relationship between pre-states and post-states. The B method extends VDM with a refinement calculus that can mechanically guide the derivation of an implementation from a top-level specification. Alloy, developed at MIT, uses relational logic and a bounded-model-checking tool called the Alloy Analyzer to check whether a specification satisfies its own constraints, making it accessible for exploring design decisions early in a project. These methods share a common goal: to replace ambiguity with structure that can be analyzed automatically. The Oxford lecture notes on formal methods in software engineering provide a concise introduction to the motivation and scope of these approaches.

Hardware Description and Assertion Languages

In digital hardware design, specification languages address the behavior of circuits across time. Hardware description languages such as VHDL and Verilog originally served as design entry tools, but their structural precision also makes them useful for behavioral specification when paired with property-checking tools. Property Specification Language (PSL), standardized as IEEE Std 1850, extends hardware description languages with a temporal logic layer that allows engineers to state properties a design must hold over simulation traces or formal models. PSL combines linear temporal logic with sequential extended regular expressions, enabling compact expressions of timing requirements such as "signal A must be followed by signal B within three clock cycles." SystemVerilog Assertions (SVA) provide a similar capability natively within SystemVerilog and are supported by most commercial electronic design automation (EDA) platforms. Both PSL and SVA are used in assertion-based verification, where properties serve as executable monitors that flag violations during simulation.

Temporal and Model-Based Specification

Temporal logic specifications, including those built on computation tree logic (CTL) and linear temporal logic (LTL), describe how a system evolves over sequences of states. Model checkers such as SPIN and NuSMV take a system model and a temporal specification as inputs, then exhaustively search the state space for a counterexample that violates the specification. The ACM Digital Library hosts a broad literature on these tools; a comparative study of formal specification approaches surveys their relative strengths for concurrent and distributed system design. State machine notations, including UML statecharts and SysML block definitions, offer a more visual specification style suited to systems engineering contexts where the audience includes non-programmers.

Applications

Specification languages have applications in a range of fields, including:

• Integrated circuit verification, where PSL and SVA properties catch RTL design bugs before fabrication
• Safety-critical software certification for avionics, medical devices, and railway control systems
• Network protocol design, where state machine specifications detect race conditions and deadlocks
• Secure system design, where formal models of access control and cryptographic protocols are checked for flaws
• Embedded systems development using model-based specification tools such as MATLAB Simulink with formal analysis add-ons