FORMAL METHOD IN Raheem ullah
SOFTWARE ENGINEERING
TODAY TOPICS :
1) Introduction of Formal Method
2) Why should we use Formal Method.
3) Industrial Application of Formal Method
4) Approaches to Formal Method
i) Model oriented Approach
ii) Axiomatic Approach or Property base approach
5) Mathematics in software Engineering
6) The Vienna Development method
FORMAL METHOD
Def 1 ) Formal specification is the use of mathematical notation to describe in a precise way the properties that
an information system must have, without unduly con- straining the way in which these properties are achieved.
Def 2 ) The formal methods model is an approach to software engineering that applies mathematical
methods or techniques to the process of developing complex software systems. The approach uses a
formal. specification language to define each characteristic of the system.
Def 3 ) Formal methods are intended to systematize and introduce rigor into all the phases of
software development. This helps us to avoid overlooking critical issues, provides a standard means to
record various assumptions and decisions, and forms a basis for consistency among many related
activities.
Goal. ) Develop a program in a way that each step leads a Final Solution, Follow proper method to make
sure that we do not take wrong steps.
FORMAL METHODS MAY BE EMPLOYED AT
A NUMBER OF LEVELS
i) Formal Specification Only (Program developed informally);
ii) Formal specification , refinement and verification (Some proofs);
iii) Formal specification, refinement and verification ( with extensive theorem proving)
WHY SHOULD WE USE
FORMAL METHODS ?
Case Study Therac-25
Radiation doses that were hundreds of
The Therac-25 machine was a state-of-the-art times greater than normal, resulting in
linear accelerator developed by the company death
or serious injury.
Atomic Energy Canada Limited (AECL) and a
French company CGR to provide radiation
treatment to cancer patients. The Therac-25 was
the most computerized and sophisticated radiation
therapy machine of its time. With the aid of an
onboard computer, the device could select
multiple treatment table positions and select the
type/strength of the energy selected by the
operating technician. AECL sold eleven Therac-25
machines that were used in the United States and
Canada beginning in 1982.
AT & T LONG DISTANCE
BREAKDOWN BUG 1990 1 while (ring receive buffer not empty
and side buffer not empty) DO
On January 15, 1990 , AT & T long distance 2 Initialize pointer to first message in side buffer
or ring receive buffer
telephone switicing system crashed. 3 get copy of buffer
4 switch (message)
Falut :: the fault was in the code " of the new 5 case (incoming_message):
software that AT & T loaded into front- end 6 if (sending switch is out of service) DO
processors of all 114 of its swithichg system. 7 if (ring write buffer is empty) DO
8 send "in service" to status map
9 else
Loss : esitmated loss of $60 million in long- 10 break
distance charges, 9 hours of service time, END IF
approximately 57 million missed phone calls, 11 process incoming message, set up pointers to
optional parameters
and a estimated loss of 200,000 airline 12 break
reservation. END SWITCH
13 do optional parameter work
PATRIOT MISSILE FAILURE
GULF WAR
On February 25, 1991 Gulf war, an america patrot
missile battery in DHARAN, saudi arbia , failed to
track and intercept an incoming iraqi scud missile.
It turns out that the cause was an inaccurate
calculation of the time since boot due to computer
arithmetic errors.
The scud struck an American Army barracks ,
Killing 28 soldiers and injuring around 100 other
people.
ARIANE 5 EXPLOSION - 1996
A European Space Agency project 10 years of
reasearch 7 billion dollors invested Exploded
within a minute
Fault : Trying to store a 64 bit float into a 16
bit integer
Loss : estimated 370 million dollors
64 bit varible represent billion of potiential
value while 16 bit represent only 65,535
potiential value.
WHY SHOULD USE FORMAL METHOD?
Formal methods help disambiguate system specifications and articulate
implicit assumptions. They also expose flaws in system requirements, and their rigor enables a better
understanding of the problem. This is why they are just a complementary technique in system design.
What is software engineering.
Solving problems
i) understand the problem
ii) Analyze the problem
Find solution.
Constructing the solution from parts that address the problem's various aspects – do a synthesis
We use different methods or techniques (formal procedures for producting a result)
Software engineering is about designing and developing high quality software
INDUSTRAIL APPLICATION OF
FORMAL METHODS
Applications. Formal methods are applied in different areas of hardware and
software, including routers, Ethernet switches, routing protocols, security
applications, and operating system microkernels such as seL4.
Tools for formal mehods :
1. VDM
2. UML/OCL
3. Hoare-Logic
4. Z notation
5. Higher order logics (HOL)
6. Axiomatic set Theory
PROPERTY BASED APPROACH
Property-based specification describes two main elements in the system; those elements are the operations
that can be performed on the system and the relationships between the operations. For example, consider a
simple instant messaging application for your cell phone. Then some operations might be:
• Start up
• Send message
Receive message
• Display message, and
• Shut down
The relationships between these operations might include:
Startup must come before any other operation.
Shut down must be the last operation performed.
Display message comes during each send message and after each receive message
MODEL ORIENTED APPROACH
Model-based specification describes the states the system can be in and how the operations can
transition the system from state to state. Consider the instant messaging application example
mentioned earlier. States the system may be in might include the very similar-sounding states:
• Starting up
• Sending message
• Receiving message
• Displaying message, and
• Shutting down
As for transitions, they might include:
Clicking the application icon to enter starting up
Or, pressing the send button to leave the sending message state
VIENNA DEVELOPMENT
METHOD (VDM)
The Vienna Development Method (VDM) is an environment for the modeling and
development of sequential software systems. The specification language of VDM has
evolved from Meta-IV, the language used at IBM’s Vienna development laboratory for
specifying the semantics of the PL/I programming language in the early 70s. The current
version of the VDM specification language, VDM-SL, has been standardized by the
International Standards Organization (ISO). It supports the modeling and analysis of
software systems at different levels of abstraction. Using VDM-SL constructs, both data
and algorithmic abstractions expressed in one level can be refined to a lower level to derive a concrete
model that is closer to the final implementation of the system.