Formal System Specification
Formal system specification involves using precise techniques
to describe, model, and verify a system. It ensures the system
is correctly implemented by meeting its given specification,
which can be defined either as a list of desirable properties
(property-oriented) or as an abstract model of the system
(model-oriented).
Formal technique
A formal technique is a mathematical method to specify a hardware
and/or software system, verify whether a specification is realizable,
verify that an implementation satisfies its specification, prove
properties of a system without necessarily running the system, etc.
The mathematical basis of a formal method is provided by the
specification language.
Formal specification language
A formal specification language consists of two sets syn and sem,
and a relation sat between them. The set syn is called the syntactic
domain, the set sem is called the semantic domain, and the relation
sat is called the satisfaction relation. For a given specification syn,
and model of the system sem, if sat (syn, sem), as shown in fig. ,
then syn is said to be the specification of sem, and sem is said to be
the specificand of syn.
sat (syn, sem)
Syntactic Domains
The syntactic domain of a formal specification language consists of
an alphabet of symbols and set of formation rules to construct well-
formed formulas from the alphabet. The well-formed formulas are
used to specify a system.
Semantic Domains
Formal techniques can have considerably different semantic
domains. Abstract data type specification languages are used to
specify algebras, theories, and programs. Programming languages
are used to specify functions from input to output values. Concurrent
and distributed system specification languages are used to specify
state sequences, event sequences, state-transition sequences,
synchronization trees, partial orders, state machines, etc.
Satisfaction Relation
Given the model of a system, it is important to determine whether an
element of the semantic domain satisfies the specifications. This
satisfaction is determined by using a homomorphism known as
semantic abstraction function. Two broad classes of semantic
abstraction functions are defined: those that preserve a system’s
behavior and those that preserve a system’s structure.
Model-oriented vs. property-oriented approaches
Formal methods are usually classified into two broad categories –
model – oriented and property – oriented approaches. In a model-
oriented style, one defines a system’s behavior directly by
constructing a model of the system in terms of mathematical
structures such as tuples, relations, functions, sets, sequences, etc.
In the property-oriented style, the system's behavior is defined
indirectly by stating its properties, usually in the form of a set of
axioms that the system must satisfy.
Example:-
Let us consider a simple producer/consumer example. In a property-
oriented style, it is probably started by listing the properties of the
system like: the consumer can start consuming only after the
producer has produced an item, the producer starts to produce an
item only after the consumer has consumed the last item, etc. A good
example of a producer-consumer problem is CPU-Printer
coordination. After processing of data, CPU outputs characters to the
buffer for printing. Printer, on the other hand, reads characters from
the buffer and prints them. The CPU is constrained by the capacity
of the buffer, whereas the printer is constrained by an
empty buffer. Examples of property-oriented
specification styles are axiomatic specification and algebraic
specification.
In a model-oriented approach, we start by defining the basic
operations, p (produce) and c (consume). Then we can state that S1
+ p → S, S + c → S1. Thus the model-oriented approaches
essentially specify a program by writing another, presumably simpler
program. Examples of popular model-oriented specification
techniques are Z, CSP, CCS, etc.
Model-oriented approaches are more suited to use in later phases of
life cycle because here even minor changes to a specification may
lead to drastic changes to the entire specification. They do not
support logical conjunctions (AND) and disjunctions (OR).
Property-oriented approaches are suitable for requirements
specification because they can be easily changed. They specify a
system as a conjunction of axioms and you can easily replace one
axiom with another one.
Merits
Encourages rigor: Creating a formal specification clarifies system behavior
and resolves ambiguities often missed in informal specifications.
Based on mathematics: Formal methods ensure precise, mathematically
sound specifications, enabling reasoning and proof of implementation
correctness.
Eliminates ambiguity: Well-defined semantics ensure clear and
unambiguous specifications.
Automation-friendly: Formal methods support automatic analysis, such as
checking specification consistency or verifying implementations using
theorem proving.
Executable specifications: Specifications can often be executed to test and
gain immediate feedback on the system's behavior.
Limitations
Difficult to learn and use: Formal methods require significant expertise and
effort.
Incomplete correctness: First-order logic's limitations mean absolute
correctness cannot always be guaranteed.
Complexity challenges: Handling complex problems is difficult as formal
methods often lead to overwhelming complexity, making large mathematical
models hard to understand.
