Advanced Software Engineering

SE-721 Spring 2024

Chapter 16
Formal Methods

Student name: Dalia Gamal

Presented to : Prof. Dr. Walid Rabie
Agenda
1. Introduction
2. Why Should We Use Formal Methods?
3. Applications of Formal Method
4. Tools for Formal Methods
5. Approaches to Formal Methods
5.1.1. Model-Oriented Approach
5.1.2. Axiomatic Approach
6. Proof and Formal Methods
7. The Future of Formal Methods

2
Agenda
8. The Vienna Development Method
9. VDM♣, the Irish School of VDM
10. The Z Specification Language
11. The B Method
12. Predicate Transformers and Weakest Preconditions
13. The Process Calculii
14. Finite State Machines
15. The Parnas Way
16. Usability of Formal Methods
17. Why are Formal Methods Difficult?
18. Characteristics of a Usable Formal Method

3
0 Introducti
1 on

4
1. Introduction

• Techniques and tools based on mathematics and formal logic

• Can assume various forms and levels of Rigor

• Focusing on the "what" rather than the "how" of a system

5
1. Introduction :cont.

Informal: Formal specification only

(program developed informally),

Low :Formal specification, refinement, and verification

(pseudocode, some proofs),

Meduim:Formal specification, refinement, and verification

(with extensive theorem proving).

6
0 Why Should We Use Formal

2 Methods?

7
2. Why Should We Use Formal
Methods?
• Identify defects earlier in life cycle ,Can guarantee the absence of certain
defects.

• Formal specification language semantics allow checks for self-consistency

of a problem specification.

• Abstract formal view helps separate specification from design.

• Enhances existing review processes by adding a degree of rigor.

• Higher level of rigor enables a better understanding of the problem.

8
0 Applications of Formal
Methods
3

9
 3. Applications of Formal
Methods

Formal methods have been used to verify the correctness of software in

various domains:

- The nuclear power industry.

- Aerospace industry.
- security technology.
- Railroad domain.

(i.e. : “when the train goes through the level crossing then the gate is closed”.)

10
0 Tools for Formal Methods
4

11
4. Tools for Formal Methods
- Formal methods have been criticized for the limited availability of tools to support
software engineers in writing formal specifications and conducting proofs.

- The tools include:

Automated code
Syntax checkers Specialized editors
generators
Specification animation Refinement support
Theorem provers
tools tools

12
4. Tools for Formal Methods:cont.

- The B-Toolkit5 from B-Core.

- The IFAD Toolbox6 is a support tool for the VDM-SL specification language .

- The Overture Integrated Development Environment (IDE) is an open-source tool for formal
modelling and analysis of VDM-SL specifications.

13
0 Approaches to Formal
Methods
5

14
5. Approaches to Formal Methods
Two key approaches to formal methods

• Model-oriented approach as VDM or Z

• Algebraic or axiomatic approach as the process calculi

Such as :

Calculus communicating systems (CCS)

Communicating sequential processes (CSP)

15
5.1. Model-Oriented Approach

• Based on mathematical models that simplify or abstract the real world by focusing
on essential details.

• Models serve to explain the behavior of a particular entity and can be used to
predict future behavior.

For example:
The model of an aircraft will not include the color of the aircraft, and the objective would be to
model the aerodynamics of the aircraft.

16
 5.1. Model-Oriented Approach:
Cont.

• The principle of "Ockham's Razor" suggests selecting the simplest model with the
fewest assumptions required.

• Ex: Copernican model of the universe replaced the older Ptolemaic model
• Various models have been applied to assist with the complexities in software development.
The Capability Maturity Model (CMM),
Unified Modeling Language (UML),
Mathematical models

https://www.techtarget.com/searchsoftwarequality/definition/Capability-Maturity-Model
17
5.2. Axiomatic Approach

• The required properties and behavior of the system are stated in mathematical
notation.

• The axiomatic approach focuses on the properties that the proposed system is to
satisfy, without producing an abstract model of the system.

18
5.2. Axiomatic Approach: cont.
• The difference between the axiomatic specification and a model-based approach
may be seen in the example of a stack.

• The stack includes operators for pushing an element onto the stack and popping
an element from the stack.

• The properties of pop and push are explicitly defined in the axiomatic approach.

• The model-oriented approach constructs an explicit model of the stack, The model
can be implemented using various data structures such as arrays, linked lists, or
dynamic arrays.

• The axiomatic specification of the pop operation on a stack is given by properties,

for example, pop(push(s, x)) = s.

19
0 Proof and Formal Methods
6

20
6. Proof and Formal Methods

• A mathematical proof consists of natural language and mathematical symbols,

with many tedious details often omitted.

• The "divide and conquer" technique is commonly used in proofs.

• Machine proofs are explicit but can be lengthy and unreadable.

• proofs by hand are prone to errors or jumps in reasoning.

• Formal methods provide increased confidence in software correctness rather than

absolute proof.

21
0 The Future of Formal
Methods
7

22
7. The Future of Formal Methods
• The debate about the use of mathematics in software engineering is ongoing.

• They argue that the use of formal mathematical techniques would impact time to
market and market opportunity.

• On the other hand, some argue that mathematics is essential for delivering high-
quality and reliable software.

• Mathematics is generally accepted to play a role in safety-critical and security-

critical fields.

23
0 The Vienna Development
Method
8

24
8. The Vienna Development
Method
• The Vienna Development Method (VDM) originated from work done by the IBM
research laboratory in Vienna.

• where they were specifying the semantics of the PL/1 programming language
using an operational semantic approach.

• Means providing a formal description of how the language constructs are intended to be
understood and executed.

• Each phrase of the language is associated with a mathematical object, such as a

set or a function and how they interact with each other.

25
8. The Vienna Development
Method: cont.
• VDM is a model-oriented approach that involves giving an explicit model of the
state of an abstract machine

• Structured into modules, which contain the module name, parameters, types,
operations.

• Allows for the refinement steps to obtain an executable specification or detailed

code.

• VDM uses keywords like "pre" and "post" to distinguish different parts of the
specification, such as preconditions and post-conditions.

26
8. The Vienna Development
Method: cont.
pre-conditions:
define the requirements that must be met before a
method is executed.

post-conditions:
describe the expected state or behavior after the
method has completed its task.

27
0 VDM♣, the Irish School of
VDM
9

28
9.VDM♣, the Irish School of VDM

• The Irish School of VDM is a variant of standard VDM that combines the what and
how of formal methods.

• The specifications are constructive, meaning that the how is included with the
what.

• Focusing on data and how it interacts with functions.

29
1 The Z Specification Language
0

30
10. The Z Specification Language
• Is a formal specification language used for describing and modeling computing
systems.

• It was developed by Jean-Raymond Abrial at Oxford University in the early 1980s.

• Z is based on Zermelo set theory and employs a classical two-valued logic.

• The Z specification language includes a mathematical notation similar to VDM .

• The Z specification language was published as an ISO standard in 2002.

• Z specifications are highly readable due to decomposing a specification into

smaller pieces.

31
10. The Z Specification Language:
cont.

• The schema calculus consists essentially of boxes, with these boxes or schemas
used to describe operations and states.

• The schemas may be used as building blocks and combined with other schemas.

• Operations are defined in a precondition/postcondition style.

• The precondition is implicitly defined within the operation.

32
10. The Z Specification
Language:cont.

Definition

invariante

Neso Academy.org
33
1 The B Method
1

34
11. The B Method

• The B-Technologies consist of three components:

B-Method B-Toolkit B-Tool

• A model-oriented approach closely related to the Z specification language.

• Each operation has an explicit precondition.

• The abstract machine in the B-Method provides encapsulation of variables

representing the state of the machine and operations that manipulate the state.

35
11. The B Method:Cont.
• The B-Method adopts a layered approach to design, with each design layer being a
refinement that involves a more detailed implementation.

• The B-Toolkit provides several tools that support the B-Method, including

syntax and type proof obligation

auto prover
checking generator
proof
specification animation code generation
assistor

● Customer Information Control System :Online Transaction Processing, Transaction

Management, Application Server…

36
1 Predicate Transformers and
Weakest Preconditions
2

37
12. Predicate Transformers and
Weakest Preconditions
{Q} S {R}
How it Works:
The Hoare triple {Q} S {R} expresses a logical relationship between the program's starting and ending
states.
If the precondition Q is true before running the program segment S,
Then the program will execute and terminate in a finite amount of time (not get stuck in an infinite
loop),
And the postcondition R will be true after the execution finishes

D. Gries, The Science of Programming (Springer, Berlin, 1981) , Chapter 7. The Predicate Transformer wp
38
12. Predicate Transformers and
Weakest Preconditions: cont.
Predicate Transformers:

• Is a function that takes a program statement (S) and a postcondition (R) as input, and returns
a precondition (P).

• In simpler terms, it takes a desired outcome (what you want the program to achieve) and tells
you what initial condition (precondition) is necessary for the program to guarantee that
outcome.
wp(S, R) = P
Here's the notation for a predicate transformer:

• This reads as: "the weakest precondition (wp) for program S to achieve postcondition R is
precondition P."

39
12. Predicate Transformers and
Weakest Preconditions: cont.
Example:
Imagine a program statement S that increments a variable x.
If the desired post condition (R) is x > 5, the predicate transformer would tell you the
weakest precondition (P) is x >= 5.
This means, as long as x is initially greater than or equal to 5, incrementing it will
guarantee x becomes greater than 5.

40
1 The Process Calculii
3

41
13. The Process Calculii

• The objectives of process calculi are to provide mathematical models for

understanding the specification, design, and implementation of computer systems
that interact with their environment .
• CSP (Communicating Sequential Processes)

C.A.R. Hoare, Communicating Sequential Processes (Prentice Hall International Series in Computer Science, 1985
42
 13. The Process Calculii:cont.
Calculus of Communicating Systems
Representation of the vending machine in CCS:
used to model concurrent systems. Both offer ways to describe how processes interact and
communicate with each other.

•A comparison of CSP and CCS: https://static.aminer.org/pdf/PDF/000/267/454/on_the_relationship_of_ccs_and_csp.pdf

•An introduction to CCS:
https://www.sciencedirect.com/science/article/pii/S1571066110000812/pdf?md5=5f3eae9bf2d943a14890a99a9276856c&pid=1-s2.0-S1571066110000812-main.pd
f

43
1 Finite State Machines
4

44
14. Finite State Machines

A finite state machine (FSM):

is an abstract mathematical machine that consists of a finite number of states.

Finite
Automata

FA with FA without
output output

Moore Mealy DFA NFA E-NFA

45
14. Finite State Machines:cont.
DFA: Deterministic Finite Automata
Every state is defined by (q, Σ,q0,f, δ)
Q={A,B,C,D}
Σ={0,1}
q-note={A}
F={D}
Δ= Qx

Nesoacademy.org

46
14. Finite State Machines: cont.
Moore Machine
t state Next state output

B0 ,b1 0 r r 00
t=0
t=0 1 r g 01
t=1
red green 0 g g 01

1 g y 10
Red: 00
Green: 01 0 y y 10
t=1 t=1 Yellow: 10
yellow 1 y r 00

t=0 Output directly from the state

Timer! : input:t
47
 t tr state Next polution
14. Finite State Machines:cont. 0 0 stop
state
stop 0
Mealy Machine
0 0 go go 0

1x/0 0 1 stop stop 1

00/0
01/1 Stop = 0 0 1 go go 0
0x/0
Go = 1
1 0 stop go 0
stop go
Input
1 0 go go 0
Timer! : t
1x/0 Trucks waiting = tr
1 1 stop go 0
Output = pollution
1 1 go stop 0

Output depends on the value of input

48
14. Finite State Machines: cont.
Turing Machine

• Is a mathematical model of computation describing an abstract machine that

manipulates symbols on a strip of tape according to a table of rules.

• a theoretical model of computation that was introduced by Alan Turing in the 1930s

• Despite the model's simplicity, it is capable of implementing any computer

algorithm

• They are primarily used as a theoretical tool for understanding the limits and
capabilities of computation.

Guide to Discrete Mathematics An Accessible Introduction to the History, Theory, Logic and Applications
https://en.wikipedia.org/wiki/
49
Turing_machine&ved=2ahUKEwiGqLCa0aOHAxV5UaQEHZGpALgQFnoECBcQAw&usg=AOvVaw08WOlU22lE8j4Aw8Zz0Qs
 Turing Machine Example:

$ a a b b c c ˽ ˽ …..

x->R
B->R A->L
A->R
B->L
$->R A->x,R b>x,R C->x,L c->L
$ back

$->R

Turing Machine Example: a^n b^n c^n (youtube.com)

50
1 The Parnas Way
5

51
15. The Parnas Way
• David Parnas has been influential in the computing field and his ideas on the
specification, design, implementation, maintenance, and documentation of
computer software remain important.

• The role of the engineer is to apply scientific principles and mathematics to design and
develop products

• Parnas believes that computer scientists need to be educated as engineers to

ensure that they have the appropriate background to build software correctly.

52
15. The Parnas Way:Cont.
His contributions to software engineering :

Area Contribution

Tabular expressions These are mathematical tables for specifying

requirements and enable complex predicate logic
expressions to be represented in a simpler form
Mathematical the use of mathematical documentation for requirements
documentation and design

Requirements specification the use of mathematical relations to specify the

requirements precisely

53
15. The Parnas Way:Cont.
Area Contribution

Software design He developed information hiding that is used in object-oriented

design a , and allows software to be designed for change. Every
information-hiding module has an interface that provides the only means to
access the services provided by the modules. The interface hides the
module’s implementation (Encapsulation)
Software inspections His approach requires the reviewers to take an active part in the inspection.

Predicate logic These are mathematical tables for specifying requirements and enable
complex predicate logic expressions to be represented in a simpler form.
state transition table for a finite state machine [FSM].

54
1 Usability of Formal Methods
6

55
16. Usability of Formal Methods
• There are practical difficulties associated with the industrial use of formal
methods.

• Programmers and customers are not always willing to become familiar with the
mathematics used in formal methods.

• The use of mathematics in formal methods is often seen as an alien activity by

customers.

• Programmers are generally more interested in programming than in mathematics

and are not interested in becoming mathematicians.

56
17.Why are formal methods difficult?
Factor Description

Notation/intuition FM notation often differs from traditional mathematical notation, and

many programmers find it unintuitive
Formal specification It is easier to read a formal specification than to write one

Validation of formal using proof techniques like inspection is difficult

specification
Refinement Refinement step is difficult and time consuming

Proof Proof can be difficult and time consuming

Tool support Many of the existing tools are difficult to use

57
 Review Questions
1. What are formal methods and describe their potential benefits? How essential is tool
support?
2. What is stepwise refinement and how realistic is it in mainstream software
engineering?
3. Discuss Parnas’s criticisms of formal methods and discuss whether his views are valid.
4. Discuss the applications of formal methods and which areas have benefited most from
their use? What problems have arisen?
5. Describe a technology transfer path for the deployment of formal methods in an
organization.
6. Explain the difference between the model-oriented approach and the axiomatic
approach.
7. Discuss the nature of proof in formal methods and tools to support proof.
8. Discuss the Vienna Development Method and explain the difference between standard
VDM and VDM♣.
58
9. Discuss Z and B.
Resources
● https://xperti.io/blogs/encapsulation/
● C.A.R. Hoare, Communicating Sequential Processes (Prentice Hall International Series in Computer Science, 1985
● Neso Academy.org
● A comparison of CSP and CCS: https://static.aminer.org/pdf/PDF/000/267/454/on_the_relationship_of_ccs_and_csp.pdf
● An introduction to CCS: https://www.sciencedirect.com/science/article/pii/S1571066110000812/pdf?
md5=5f3eae9bf2d943a14890a99a9276856c&pid=1-s2.0-S1571066110000812-main.pdf
● Guide to Discrete Mathematics An Accessible Introduction to the History, Theory, Logic and Applications
● https://
en.wikipedia.org/wiki/Turing_machine&ved=2ahUKEwiGqLCa0aOHAxV5UaQEHZGpALgQFnoECBcQAw&usg=AOvVaw08WOlU22
lE8j4Aw8Zz0Qs
● Turing Machine Example: a^n b^n c^n (youtube.com)
● https://www.techtarget.com/searchsoftwarequality/definition/Capability-Maturity-Model
● Finite State Machines explained (youtube.com)
● Neso Academy.org
● Concise Guide to Software Engineering From Fundamentals to Application Methods

59
Thank You

60