Transcript Formal methods Formal specification

Formal Specification - Techniques for the
unambiguous specification of software
Objectives:


To explain why formal specification techniques
help discover problems in system requirements
To describe the use of
•
•

algebraic techniques (for interface specification) and
model-based techniques(for behavioural specification)
To introduce Abstract State Machine Model
Slide 1
Formal methods


Formal specification is part of a more general
collection of techniques that are known as
‘formal methods’
These are all based on mathematical
representation and analysis of software
Formal methods include
•
•
•
•
Formal specification
Specification analysis and proof
Transformational development
Program verification
Slide 2
Notations For Formal Specification




Any notation with precise semantics can be used
Formalism typically applied to just part of a
specification
Notations use discrete mathematics, some with
graphics
Several notations are sometimes used in the
same specification:
•
•
•
Z or VDM for data manipulation
Statecharts for system states and transitions
Natural language for non-functional specifications
Slide 3
Formal Specification

Goals of formal specification:
•
•
•
•
•



Complete
Consistent
Concise
Unambiguous
Valid—state exactly what the user wants
Specifications based on formal semantic model
What is/are semantics?
What is a formal semantic model?
Slide 4
Formal Semantics


Semantics means “meaning”
Formal semantics:
•

Formal semantic model:
•

Complete semantic definition of a language in mathematics
What mathematics?
•

Meaning expressed in mathematics
Discrete mathematics!
Formal semantics permit dependable
communication between all parties
Slide 5
Types Of Languages

Procedural:
•
•

Declarative:
•
•

Computation defined by desired sequence of actions computer is to
perform
Most high-level languages are procedural
Computation defined by desired state that computer should be in
Many specification languages are declarative
Functional:
•
•
Computation defined as desired function computer is to evaluate
Most functional languages derive from LISP
Slide 6
Types Of Languages

High-level language programs are actually
specifications!
•
•

Compilers write the program for you
So you have been specifying programs, not writing them
The big difference in languages is:
•
Declarative:
» Says nothing about HOW, just WHAT
•
Procedural:
» Says nothing about WHAT, just HOW
Slide 7
Types Of Languages—Examples


Procedural:
read (x);
y := x;
while y**2 > x loop
y := y – 1;
end loop;
print (y);
Declarative:
y**2 <= x AND (y+1)**2 > x
Slide 8
Formal Methods Activities


Write a specification using a formal notation
Validate the specification
•
•

Refine the specification to an implementation
•

Inspect it with domain experts
Perform automated analysis to prove theorems
Semantics-preserving transformations to code
Verify that the implementation matches the spec
•
Mathematical argument
Slide 9
Library Example: Informal
Statement



A book can either be in the stacks, on reserve, or
loaned out
If a book is in the stacks or on reserve, then it
can be requested
We want to
•
•
formalize the concepts and the statements
prove some theorems to gain confidence that the spec is
correct
Slide 10
Library Example: Formalization
(1/2)





First let’s formalize some concepts
S: the book is in the stacks
R: the book is on reserve
L: the book is on loan
Q: the book is requested
Slide 11
Library Example: Formalization
(2/2)
If a book is requested, then it is on the shelf or
on reserve
Slide 12
Library Example: Proof of a
Theorem
Slide 13
Library Example: Proof By
Contradiction
Slide 14
Use of formal methods

Their principal benefits are in reducing the number of
errors in systems so their main area of applicability is
critical systems:
•
•
•
•


Air traffic control information systems,
Railway signalling systems
Spacecraft systems
Medical control systems
In this area, the use of formal methods is most likely
to be cost-effective
Formal methods have limited practical applicability
Slide 15
Use of formal specification


Formal specification involves investing more
effort in the early phases of software
development
This reduces requirements errors as it
forces a detailed analysis of the requirements
Incompleteness and inconsistencies can be
discovered and resolved !!!
Hence, savings as made as the amount of
rework due to requirements problems is
reduced
Slide 16
Acceptance of formal methods

Formal methods have not become mainstream
software development techniques as was once
predicted
•
•
•
•
Other software engineering techniques have been successful at
increasing system quality. Hence the need for formal methods
has been reduced
Market changes have made time-to-market rather than software
with a low error count as the key factor. Formal methods do not
reduce time to market
The scope of formal methods is limited. They are not well-suited
to specifying and analysing user interfaces and user interaction
Formal methods are hard to scale up to large systems
Slide 17
Two specification techniques

Algebraic approach
•

The system is specified in terms of its operations and
their relationships
Model-based approach
•
•
The system is specified in terms of a state model that
is constructed using mathematical constructs such
as sets and sequences.
Operations are defined by modifications to the
system’s state
Slide 18
Interface specification



Large systems are decomposed into subsystems
with well-defined interfaces between these
subsystems
Specification of subsystem interfaces allows
independent development of the different
subsystems
Interfaces may be defined as abstract data types
or object classes
The algebraic approach to formal
specification is particularly well-suited to
interface specification
Slide 19
Sub-system interfaces
Interface
objects
Sub-system
A
Sub-system
B
Slide 20
The structure of an algebraic
specification
< SPECIFICATION NAME > (Generic Parameter)
sort < name >
imports < LIST OF SPECIFICATION NAMES >
Informal descr iption of the sor t and its operations
Operation signatures setting out the names and the types of
the parameters to the operations defined over the sort
Axioms defining the operations over the sort. Axioms relate
the operations used to construct entities with operations used
to inspect their values.
Slide 21
Specification components

Introduction
•

Description
•

Informally describes the operations on the type
Signature
•

Defines the sort (the type name) and declares other
specifications that are used
Defines the syntax of the operations in the interface and
their parameters
Axioms
•
Defines the operation semantics by defining axioms which
characterise behaviour
Slide 22
Specification operations



Constructor operations. Operations which
create entities of the type being specified
Inspection operations. Operations which
evaluate entities of the type being specified
To specify behaviour, define the inspector
operations for each constructor operation
Slide 23
Interface specification in critical
systems




Consider an air traffic control system where aircraft
fly through managed sectors of airspace
Each sector may include a number of aircraft but, for
safety reasons, these must be separated
In this example, a simple vertical separation of 300m
is proposed
The system should warn the controller if aircraft are
instructed to move so that the separation rule is
breached
Slide 24
A sector object

Critical operations on an object representing
a controlled sector are
•
•
•
•
Enter. Add an aircraft to the controlled airspace
Leave. Remove an aircraft from the controlled airspace
Move. Move an aircraft from one height to another
Lookup. Given an aircraft identifier, return its current
height
Slide 25
Primitive operations



It is sometimes necessary to introduce additional
operations to simplify the specification
The other operations can then be defined using these
more primitive operations
Primitive operations
•
•
•
•
Create. Bring an instance of a sector into existence
Put. Add an aircraft without safety checks
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
Slide 26
Slide 27
Behavioural specification


Algebraic specification can be
cumbersome when the object operations
are not independent of the object state
Model-based specification exposes the
system state and defines the operations in
terms of changes to that state
Slide 28
Abstract State Machine
Language (AsmL)


AsmL is an executable specification language
for modelling the structure and behaviour of
digital systems
AsmL can be used to faithfully capture the
abstract structure and step-wise behaviour of
any discrete systems, including very complex
ones such as:
Integrated circuits, software components, and devices that combine
both hardware and software
Slide 29
Abstract State


An AsmL model is said to be abstract because it
encodes only those aspects of the system’s structure
that affect the behaviour being modelled
The goal is to use the minimum amount of detail
that accurately reproduces (or predicts) the
behaviour of the system
Abstraction helps us reduce complex problems into
manageable units and prevents us from getting lost in a
sea of details
AsmL provides a variety of features that allow you to
describe the relevant state of a system in a very
economical, high-level way
Slide 30
Abstract State Machine and
Turing Machine



An abstract state machine is a particular
kind of mathematical machine, like the
Turing machine (TM)
But unlike a TM, ASMs may be defined a
very high level of abstraction
An easy way to understand ASMs is to see
them as defining a succession of states
that may follow an initial state
Slide 31
State transitions

The behaviour of a machine (its run) can always
be depicted as a sequence of states linked by
state transitions
paint in green
A
paint in red
B
• Moving from state A to state B is a state
transition
Slide 32
Configurations



Each state is a particular “configuration” of
the machine
The state may be simple or it may be very
large, with complex structure
But no matter how complex the state might
be, each step of the machine’s operation can
be seen as a well-defined transition from
one particular state to another
Slide 33
Evolution of state variables
We can view any machine’s state as a dictionary of
(Name, Value)
pairs, called state variables
paint in green
A
paint in red
B
(Colour, Red) is a variable, where “Colour” is
the name of variable, “Red” is the value
Slide 34
Evolution of state variables


Names are given by the machine’s symbolic
vocabulary
Values are fixed elements, like numbers and
strings of characters
The run of a machine is a series of
states and state transitions that
results form applying operations
to each state in succession
Slide 35
Example
Diagram shows the run of a machine that models how orders might be
Initialise
Process All Orders
processed
S1
S2
S3
Mode = “Initial”
Mode = “Active”
Mode = “Final”
Orders = 0
Orders = 2
Orders = 0
Balance = £0
Balance = £200
Balance = £500
Each transition operation:
• can be seen as the result of invoking the machine’s
control logic on the current state
• calculates the subsequence state as output
Slide 36
Control Logic
The machine’s control logic
behaves like a fix set of transition
rules that say how state may evolve
Typical form of the operational text is:
“ if condition then update ”
We can think of the control logic as a text that
precisely specifies, for any given state, what the
values of the machine’s variables will be in the
following step
Slide 37
Control Logic as a Black Box
• The machine control logic is a black box that takes as input a
state dictionary S1 and gives as output a new dictionary S2
mode
“Initial”
orders
0
balance
£0
input
The Machine’s Control
Logic
output
…
Mode
“Active”
orders
2
balance
£200
if mode = “Initial”
then mode := “Active”

The two dictionaries S1 and S2 have the same set of
keys, but the values associated with each variable
name may differ between S1 and S2
Slide 38
Run of the Machine


The run of the machine can be seen as what happens
when the control logic is applied to each state in turn
The run starts form initial state
S1  S2  S3  …
S1 is given to the black box yielding S2, processing S2 results in S3,
and so on …

When no more changes to state are possible, the run is
complete
Slide 39
Update operations


We use the symbol
“: =” (reads as “gets”)
to indicate the value that a name will have in the
resulting state
For example: mode:=“Active”
Update can be seen only during the following step
(this is in contrast to Java, C, Pascal, …)

All changes happen simultaneously, when you
moving from one step to another. Then, all
updates happen at once.(atomic transaction)
Slide 40
Programs
Example 1. Hello, world
Main()
step WriteLine(“hello, world!”)
ASML uses indentations to denote block structure, and blocks can
be places inside other blocks
Statement block affect the scope of variables
Whitespace includes blanks and new-line character, ASML does not
recognize tab character for indentation !!!!!!!
Main() is like main() in Java and C
Slide 41
Example 2. Reading a file
var F as File? = undef
var Fcontents as String = “”
var Mode as String = “Initial”
Main()
step until fixpoint
if Mode = “Initial” then
F :=open(“mfile.txt”)
Mode :=“Reading”
if Mode = “Reading” and length(FContents) =0 then FContents :=fread (F,1)
if Mode = “Reading” and length(FContents) =1 then
FContents := FContents + fread (F,1)
if Mode = “Reading” and length(FContents) >1 then
WriteLine (FContents)
Mode :=“Finished”
Slide 42
Example 2.
Graph representation
Step 1
Step 2
S1
S2
S3
F= undef
F= <open file 1>
F= <open file 1>
Fcontents =“”
Fcontents =“”
Fcontents =“a”
Mode = Initial
Mode = Reading
Mode = Reading
Step 3
S4
S5
F= <open file 1>
F= <open file 1>
Fcontents =“ab”
Fcontents =“ab”
Mode = Reading
Step 4
Mode = Finished
Slide 43
Step5
Key points



Formal system specification complements
informal specification techniques
Formal specifications are precise and
unambiguous. They remove areas of doubt in a
specification
Formal specification forces an analysis of the
system requirements at an early stage.
Correcting errors at this stage is cheaper than
modifying a delivered system
Slide 44
Key points



Formal specification techniques are most
applicable in the development of critical systems
and standards.
Algebraic techniques are suited to interface
specification where the interface is defined as a
set of object classes
Model-based techniques model the system using
sets and functions. This simplifies some types of
behavioural specification
Slide 45