Formal Specification Objectives

• To explain why formal specification

techniques help discover problems in
• Techniques for the system requirements
unambiguous • To describe the use of algebraic
techniques for interface
specification of specification
software • To describe the use of model-based
techniques for behavioural
specification

Topics covered Formal methods

• Formal specification in the software • Formal specification is part of a more
process general collection of techniques that are
known as ‘formal methods’
• Interface specification
• These are all based on mathematical
• Behavioural specification representation and analysis of software
• Formal methods include
– Formal specification
– Specification analysis and proof
– Transformational development
– Program verification

Acceptance of formal methods Use of formal methods

• Formal methods have not become • Their principal benefits are in
mainstream software development reducing the number of errors in
techniques as was once predicted systems so their main area of
– Other software engineering techniques have
been successful at increasing system quality.
applicability is critical systems
– Market changes have made time-to-market • In this area, the use of formal
rather than software with a low error count methods is most likely to be cost-
the key factor. Formal methods do not
reduce time to market effective
– Formal methods are hard to scale up to large
systems

1
 Specification in the software
process Specification and design
• Specification and design are Requirements
Requirements
intermingled. Definition
Definition

• Architectural design is essential to Requirements

Requirements
structure a specification. Specification
Specification
In
• Formal specifications are expressed cr
e
De asin Architectural
Architectural
cr
in a mathematical notation with ea g Co Design
Design
s in n t
g C rac
precisely defined vocabulary, syntax lie tor
nt I
In nvo Software
Software
and semantics. Specification
vo
lve lvem Specification
Specification
me en
nt t
High-level
High-level
Design
Design
Design

Specification in the software

Specification techniques
process
• Algebraic approach
Requirements Formal
– The system is specified in terms of its
Requirements Formal
Specification
Specification Specification
Specification
operations and their relationships
• Model-based approach
Requirements
Requirements High-level
High-level – The system is specified in terms of a
Definition
Definition Design
Design
state model that is constructed using
System
System Architectural
Architectural mathematical constructs such as sets
Modeling
Modeling Design
Design and sequences. Operations are defined
by modifications to the system’s state

Formal specification languages Use of formal specification

• Formal specification involves investing
Sequential Concurrent more effort in the early phases of
software development
• This reduces requirements errors as it
Algebraic Larch Lotos forces a detailed analysis of the
requirements
• Incompleteness and inconsistencies can
be discovered and resolved
Model-based 1. Z 1. CSP
• Hence, savings as made as the amount of
2. VDM 2. Petri Nets rework due to requirements problems is
3. B reduced

2
Development costs with formal specification
Interface specification
Validation • Large systems are decomposed into
Validation
subsystems with well-defined interfaces
Design &
Implementation
between these subsystems
Design & • Specification of subsystem interfaces
Implementation
allows independent development of the
Cost

different subsystems
Specification

• Interfaces may be defined as abstract

data types or object classes
Specification

• The algebraic approach to formal

specification is particularly well-suited to
Without formal specification With formal specification interface specification

The structure of an algebraic

Sub-system interfaces specification
Interface
<Specification Name> (Generic Parameter)
objects
Sort
Sort <name>
<name>
Imports
Imports <list
<list of
of specification
specification names>
names>
Sub-system
Sub-system Sub-system
Sub-system Informal
Informal description
description of
of the
the sort
sort and
and its
its operations
operations
AA BB
Operation
Operation signatures
signatures setting
setting out
out the
the names
names and
and the
the
types
types of
of the
the parameters
parameters toto the
the operations
operations defined
defined
over the sort
over the sort
Axioms
Axioms defining
defining the
the operations
operations over
over the
the sort
sort

Systematic algebraic
Specification components
specification
• Introduction • Algebraic specifications of a system
– Defines the sort (the type name) and may be developed in a systematic
declares other specifications that are used
• Description way
– Informally describes the operations on the – Specification structuring.
type – Specification naming.
• Signature
– Operation selection.
– Defines the syntax of the operations in the
interface and their parameters – Informal operation specification
• Axioms – Syntax definition
– Defines the operation semantics by defining – Axiom definition
axioms which characterise behaviour

3
 Interface specification in critical
Specification operations systems
• Constructor operations. Operations • Consider an air traffic control system
where aircraft fly through managed
which create entities of the type
sectors of airspace
being specified • Each sector may include a number of
• Inspection operations. Operations aircraft but, for safety reasons, these
which evaluate entities of the type must be separated
being specified • In this example, a simple vertical
separation of 300m is proposed
• To specify behaviour, define the • The system should warn the controller if
inspector operations for each aircraft are instructed to move so that
constructor operation the separation rule is breached

A sector object Primitive operations

• Critical operations on an object • It is sometimes necessary to introduce
representing a controlled sector are additional operations to simplify the
specification
– Enter. Add an aircraft to the
controlled airspace • The other operations can then be
defined using these more primitive
– Leave. Remove an aircraft from the
operations
controlled airspace
• Primitive operations
– Move. Move an aircraft from one
– Create. Bring an instance of a sector into
height to another existence
– Lookup. Given an aircraft identifier, – Put. Add an aircraft without safety checks
return its current height – In-space. Determine if a given aircraft is in
the sector
– Occupied. Given a height, determine if there
is an aircraft within 300m of that height

Specification commentary
SECTOR
Sector sort Sector
imports INTEGER, BOOLEAN

specification Enter - adds an aircraft to the sector if safety conditions are satisfed
Leave - removes an aircraft from the sector
Move - moves an aircraft from one height to another if safe to do so
Lookup - Finds the height of an aircraft in the sector

• Use the basic constructors Create

Create - creates an empty sector
Put - adds an aircraft to a sector with no constraint checks
In-space - checks if an aircraft is already in a sector
Occupied - checks if a specified height is available

Enter (Sector, Call-sign, Height) → Sector

Leave (Sector, Call-sign) → Sector
Move (Sector, Call-sign, Height) → Sector
and Put to specify other operations
• Define Occupied and In-space using
Lookup (Sector, Call-sign) → Height

Create → Sector
Put (Sector, Call-sign, Height) → Sector
In-space (Sector, Call-sign) → Boolean

Create and Put and use them to

Occupied (Sector, Height) → Boolean
Enter (S, CS, H) =
if In-space (S, CS ) then S exception (Aircraft already in sector)

make checks in other operation

elsif Occupied (S, H) then S exception (Height conflict)
else Put (S, CS, H)
Leave (Create, CS) = Create exception (Aircraft not in sector)

definitions
Leave (Put (S, CS1, H1), CS) =
if CS = CS1 then S else Put (Leave (S, CS), CS1, H1)

Move (S, CS, H) =

if S = Create then Create exception (No aircraft in sector)

• All operations that result in changes

elsif not In-space (S, CS) then S exception (Aircraft not in sector)
elsif Occupied (S, H) then S exception (Height conflict)
else Put (Leave (S, CS), CS, H)

to the sector must check that the

-- NO-HEIGHT is a constant indicating that a valid height cannot be returned

Lookup (Create, CS) = NO-HEIGHT exception (Aircraft not in sector)

Lookup (Put (S, CS1, H1), CS) =

safety criterion holds

if CS = CS1 then H1 else Lookup (S, CS)
Occupied (Create, H) = false
Occupied (Put (S, CS1, H1), H) =
if (H1 > H and H1 - H ≤ 300) or (H > H1 and H - H1 ≤ 300) then true
else Occupied (S, H)
In-space (Create, CS) = false
In-space (Put (S, CS1, H1), CS ) =
if CS = CS1 then true else In-space (S, CS)