Formal Methods in Software

Engineering
Week # 1

Spring-2025

Instructor: Saira Latif

Today’s Agenda
Introductory Session
Course Objectives
Learning Outcomes
Administrative Items
Fundamental Concepts
Questions ?

2
Course Title: Formal Methods in Software Engineering

Instructor: Saira Latif

Lecturer, FOIT, UCP
Experience 5+ years of research and teaching
Research Areas: Software development, reverse engineering,
multilingual source code analysis, cross-language link detection,
and machine learning in software engineering.

Course contents will be available on the portal

Email for correspondence: saira.latif@ucp.edu.pk

Course Duration: 15/16 Weeks
Office Hours
Office: Office 05, C-Block
Email: saira.latif@ucp.edu.pk
Office Hours:
Tuesday: 02:00 pm to 3:30 pm
Wednesday: 11:00 am to 1:00
pm

* will be updated during the

semester if required
4
Class
Introduction

1. Name

2. Semester

3. Working experience (in any)

4. Why to Choose this course?

5. Future Plan
Overall Learning
Outcomes
 Upon completion of this course, you will be
able to:
◦ Describe the costs and benefits of formal
methods
◦ Construct formal models of sequential software
systems
◦ Implement sequential software systems based
on formal models
◦ Verify attributes of formal models
◦ Demonstrate formal correctness of simple
procedure

6
 Plagiarism Policy
Any form of cheating in assignments,
homework problems, quizzes, and
exams will result in strict action.
Plagiarism detection tools might be
used to determine who has cheated in
assignments.
All the parties involved will be awarded
Zero in the first instance.
Repeat of the same offense will result in
(F) grade.

7
Tentative Grading Policy *

Class Participation
10%
Quiz 15%
Assignments
15%
Mid Term 20%
Final 40%

8
Course Sessions

Highly Interactive !!!

9
10
What is Engineering?
 The
action of working artfully to bring
something about.

 Engineering is the use of scientific

principles to design and build hardware
and/or software to fulfill the user need.

 Engineers design, build, and maintain

various complex systems and
structures, from buildings to software.

11
12
What is Software
Engineering?
 Software engineering is the application of
principles used in the field of engineering,
which usually deals with physical systems, to
the design, development, testing, deployment
and management of software systems.

 Software engineering is a systematic

engineering approach to software
development. A software engineer is a person
who applies the principles of software
engineering to design, develop, maintain,
test, and evaluate computer software.

13
Software in Modern Life
Software has become critical to modern life
•Process Control (oil, gas, water, . . . )

•Transportation (air traffic control, . . . )

•Health Care (patient monitoring, device control . . . )

•Finance (automatic trading, bank security . . . )

•Defense (intelligence, weapons control, . . . )

•Manufacturing (precision milling, assembly, . . . )

14
Software systems are
embedded everywhere

15
Software systems are
embedded everywhere
Some of them are critical !!!

Failing software costs money and

life !!! 16
Increasing Complexity of
Software
 The average iPhone app has less than 50,000
lines of code
 Google’s entire code base is 2 billion lines of
code for all services
 Code behind machines e.g., fighter jets, popular
video game engines, and even the Large Hadron
Collider fall somewhere in between these two
extremes
 The Control Software to run a US military drone uses 3.5
million lines of code
 A Boeing 787 has 6.5 million lines of code behind its
avionics and online support systems
 Google Chrome (browser) runs on 6.7 million lines of code
 Android operating system runs on 12-15 million lines of
code
 Large Hadron Collider uses 50 million lines of code
https://informationisbeautiful.net/visualizations/million-lines-of-code/ 17
Software Failures –
Pentium Fails Long Division
(1993)
 Cost: $475 million, corporate credibility

 Disaster: Intel’s highly-promoted Pentium chip

occasionally made mistakes when dividing floating-point
numbers within a specific range. For example, dividing
4195835.0/3145727.0 yielded 1.33374 instead of 1.33382,
an error of 0.006%. Although the bug affected few users, it
become a public relations nightmare. With an estimated 5
million defective chips in circulation, Intel offered to replace
Pentium chips only for consumers who could prove they
needed high accuracy. Eventually Intel replaced the chips
for anyone who complained.

 Cause: The divider in the Pentium floating point unit had a

flawed division table, missing about five of a thousand
entries and resulting in these rounding errors.
Software Failures –
Cancer Treatment to Die For (2000)
 Cost: Eight people dead, 20 critically injured

 Disaster: Radiation therapy software by Multi-

data Systems International miscalculated the
proper dosage, exposing patients to harmful and
in some cases fatal levels of radiation. The
physicians, who were legally required to double-
check the software’s calculations, were indicted
for murder.

 Cause:The software calculated radiation dosage

based on the order in which data was entered,
sometimes delivering a double dose of radiation.
Peculiarity of Software
Systems
 Software
faults can have catastrophic
consequences:
◦ Ariane 5, Explosion (data conversion of a too large
number)
 https://www.bugsnag.com/blog/bug-day-ariane-5-disaster

◦ Mars Climate Orbiter, Loss (spurious signals that the

lander had landed)
 https://solarsystem.nasa.gov/missions/mars-climate-orbiter/in-depth/

◦ Mars Sojourner, Pathfinder (unwanted restart)

◦ Patriot–Scud (rounding error)
https://www.iro.umontreal.ca/~mignotte/IFT2425/Disasters.html

◦ Denver Airport Luggage Handling System

◦ Pentium-Bug, Division Algorithm (incomplete entries
in a look-up-table)
(more at http://www5.in.tum.de/~huckle/bugse.html)
20
Consequences of Software
Failure
Loss of Life Loss of Money
• Software used to control  Thousands of dollars for
nuclear power plants each minute of factory
down-time
• Air-traffic control systems

 Huge losses of monetary

• Spacecraft launch
vehicle control and intellectual
investment
• Embedded software in
cars  Business failures due to
buggy software
21
Real Life Projects in Other
Domains
 All branches of engineering use mathematics
to validate designs before implementation.
 For example:
◦ Civil engineers use mathematics to compute the
structural strength of bridges and buildings.
◦ Aeronautical engineers use mathematics to
evaluate different aircraft designs.

 However, software systems, although

they are among the most complex
artifacts we build, are often still built
without mathematical modeling.
22
What are Formal
Methods ?
Working Definition: Formal methods are
techniques and tools that are based on
models of mathematics and mathematical
logic and support the description,
construction and analysis of hardware and
software systems.

Aspects of Formal Methods:

• specification: build formal system models
• construction: derive correct executable code
from formal specifications
• verification: prove that models behave as
intended
23
Why to Use Formal
Methods?
Short comings of Diagram
(informal specification)
◦ Unstructured
◦ Had neither syntax nor semantics.
◦ Impossible to prove the formal
correctness of model of the system.

FM is different form Design....

How?????

29
Why to Use Formal
Methods?
Mathematical modeling and
analysis contribute to the overall
quality of the final product

Increase confidence in the

correctness / robustness /
security of a system

Find more flaws and earlier (i.e.,

during specification and design
vs. testing and maintenance)

30
Benefits of using Formal
Methods
 Forces developers to think systematically about
issues

 Improves the quality of specifications and design,

even without formal verification

 Provides a precise reference to check requirements

against

 Providesdocumentation within a team of

developers

 Providesa basis for reuse via specification

matching

 Facilitates automatic test case generation 31

Limitations of Formal
Methods
 Useformal methods as supplements to quality
assurance methods not a replacement for them

 Formalmethods can increase confidence in a

product’s reliability if they are applied skillfully

 Useful for consistency checks, but formal

methods cannot guarantee the completeness
of a specifications

 Formalmethods must be fully integrated with

domain knowledge to achieve positive results

32
Ten Commandments – I
 Choose the appropriate notation
◦ The specification language used during the initial
stages of system development shall have a well-
defined formal semantics

◦ Trade–off between the expressiveness of a

specification language and the levels of abstraction
that it supports

◦ Suitability with the system – sequential vs.

concurrent systems

◦ Well established notation with a good user base to

ensure successful application in an industrial setting

33
Ten Commandments – II
 Do not over-formalize
◦ Shouldn’t be used only to satisfy unexplained desire
of the company or as a result of peer pressure
◦ Applying formal methods to all aspects of a system
would be both unnecessary and costly e.g., UI
design falls within the domain of informal reasoning.
◦ Consider the level to which formal methods will be
employed:
 Formal language aids in making specifications more concise and
less ambiguous (Formal Specification)

 Formally specify the system under consideration, proving that

certain properties are maintained, and undesirable properties
are avoided, and finally translating abstract specification into
executable code (Formal Development / Verification)

 With support tools, mechanically check proofs for consistency

and well-foundedness (Machine-checked Proofs).

34
Ten Commandments – III
Estimate costs
◦ Formal methods are expensive when applied
extensively or for the first time

◦ Inexperience in cost estimation of using formal

methods can result in projects over-running the
budget

◦ Formal methods can result in a reduction of errors

and an increase in quality of the code produced

◦ For high integrity systems, cost of deploying formal

methods is warranted and the returns are sufficient
to justify this.

35
Ten Commandments – IV
 Have a formal methods guru on call
◦ Majority of successful formal methods projects
to date have had access to at least one
consultant who is already expert in the use of
formal techniques.

◦ At IBM, formal methods experts spent months

on-site training people and resulted in a critical
mass of expertise at the company.

◦ Could also have a pool of mathematicians and

software/system engineers who could
sufficiently communicate with each other to
ensure project success.
36
Ten Commandments – V
 Donot abandon traditional development
methods
◦ It is desirable to integrate formal methods into the
design process in a cost-effective manner.

◦ An alternate to integration is the use of formal methods

to review an existing process.

◦ Cleanroom approach is a technique that could easily

incorporate the use of existing formal notations to
produce highly reliable software by means of non
execution-based program development.

◦ Combine different formal methods together usefully and

effectively e.g., HOL (Higher Order Logic) with Z

37
Ten Commandments – VI
 Document sufficiently
◦ Formalizing the documentation leads to less ambiguity
and thus less likelihood of errors

◦ In the case of safety-critical systems, timing issues

become significant and methods for documenting these
are especially important.

◦ Formal methods provide a precise and unambiguous

way of recording the expected and delivered system
functionality, and can therefore be used as a powerful
documentation aid.

◦ It is highly recommended to produce an informal

specification to explain the formal description
38
Ten Commandments – VII
 Do not compromise quality standards
◦ Developers look on the application of formal
methods as a means of developing correct
software.

◦ On the contrary, formal methods are merely a

means of achieving higher integrity systems
when applied appropriately.

◦ There is nothing magical about formal

methods, and the organization must ensure
that it continues to satisfy its quality
standards.
39
Ten Commandments – VIII
Do not be dogmatic in assuming formal
specifications are flawless
◦ Formal methods are just one of a number of
techniques that when applied correctly have
been demonstrated to result in systems of
the highest integrity, and one should not
dismiss other methods entirely.

◦ Formal methods are no guarantee of

correctness; they are applied by humans,
who are obviously prone to error

40
Ten Commandments – IX
Use of formal methods does not eliminate
the need to test products
◦ Dijkstra highlighted that testing can demonstrate the
presence of ‘bugs’, it cannot demonstrate their absence

◦ Formal methods allow us to propose properties of the

system and to demonstrate that they hold

◦ Formal methods allow us to examine system behavior

and to convince ourselves that all possibilities have
been anticipated

◦ Formal methods enable us to prove the conformance of

an implementation with its specification

41
Ten Commandments – X
Reuse is still important
◦ Over the long term, the only rational way
to reduce software costs and increase
software quality is through reuse.

◦ Formal methods do not change this reality.

◦ In fact, it may be that formal methods are

an appropriate approach when
components for reuse libraries are to be
created.

42
Myths of Formal Methods
–I
 Myth 1: Formal Methods can guarantee that software is perfect

 Myth 2: Formal Methods are all about proving program

correctness

 Myth 3: Formal Methods are only useful for safety-critical

systems

 Myth 4: Formal Methods require highly trained mathematicians

 Myth 5: Formal Methods increase the cost of development

 Myth 6: Formal Methods are unacceptable to users

 Myth 7: Formal Methods are not used on real, large-scale

software
43
Myths of Formal Methods
– II
 Myth 8: Formal Methods delay the development process

 Myth 9: Formal Methods lack tools

 Myth 10: Formal Methods replace traditional

engineering design methods
 Myth 11: Formal Methods only apply to software (and
not to hardware)
 Myth 12: Formal Methods are unnecessary

 Myth 13: Formal Methods are not supported

 Myth 14: Formal Methods people always use formal

methods
44
 Formal methods vs
Testing
 Traditional system design has used extensive testing to verify behavior,
but testing is capable of only finite conclusions. Dijkstra and others
have demonstrated that tests can only show the situations where a
system won't fail, but cannot say anything about the behavior of the
system outside of the testing scenarios. In contrast, once a theorem is
proven true it remains true.

 It is very important to note that formal verification does not remove the
need for testing. Formal verification cannot fix bad assumptions in the
design, but it can help identify errors in reasoning which would
otherwise be left unverified. In several cases, engineers have reported
finding flaws in systems once they reviewed their designs formally.
Formal Specification
Languages
A formal specification language
consists of
–syntax (the notation)
–semantics (the meaning)
–satisfies (relation defining which objects satisfy which
notations)

A formal specification defines

–syntax (signature of the mapping)
–semantics (meaning of the mapping)
–exceptions (undefined/erroneous mappings)

46
Formal Specifications are not
yet widely used
Reasons
–emerging technology with unclear payoff
–little experience
–not especially user friendly

Excuses
–high learning curve
–mathematical sophistication required
–techniques not widely applicable
–ignorance of advances

47
Formal Specification in
Software Development
Formalspecifications ground the software
development process in the well-defined basis of
computer science

Emphasis switches from customer to developer

Formal specification expressed in language

whose syntax and semantics are formally
defined
–hierarchical decomposition
–mathematical foundation
–graphical presentation
–accompanied by informal description
I

48
Goals and Objectives
Requirements Specification
–clarify customer's requirements
–reveal ambiguity, inconsistency, incompleteness
System/Software Design
–decomposition structural specifications of component
relations and behavioural specification of components
–refinement demonstrating that next level of abstraction
satisfies higher level
Verification

–proving a specificand (implementation) satisfies its

specification
Validation

–testing and debugging

Documentation

–communication between specifier, implementor,

customer, clients
49
Weakness of Natural
Language specification
Incomplete Specification
Inconsistent Specification
Formal Languages
Formal Methods
Three Levels of Formal
Methods
Formal Specification
Methods
Conclusion