Formal methods mathematical languages, techniques and tools, used to specify and verify systems, goal is help engineers construct more reliable systems. Introduction to Formal Methodspresents about introduction; formal specification; formalformal verificationverification; model checking; theorem proving.
Introduction (cid:132) Introduction (cid:132) Formal Specification (cid:132) Formal Verification (cid:132) Formal Verification (cid:132) Model Checking (cid:132) Theorem Proving
Good papers to begin with them: (cid:132) Good papers to begin with them: (cid:133)“Formal Methods: State of the Art and Future Directions”, Edmund M. Clarke, Jeannette M. Wing, ACM Computing Surveys, 1996
(cid:133)“Ten Commandments of Formal Methods ... Ten Years Later”, Jonathan P., Bowen and Mike Hinchey, IEEE Computer, 39(1):40-48, January 2006. 2006 J
, ,
Teaching to unsuspecting youngsters the effective use of formal methods is the effective use of formal methods is one of the joys of life because it is so extremely rewarding extremely rewarding
“The Cruelty of Really Teaching Computing
Science is a 1988 paper by E. W. Dijkstra, Science” is a 1988 paper by E. W. Dijkstra,
A more mathematical approach is inevitable. Professional software development—not the everyday brand practiced by the public at large will become more like a true engineering large—will become more like a true engineering discipline, applying mathematical techniques. I don't know how long this evolution will take, but it will happen. The basic theory is there, but much work remains to make it widely applicable. (Bertrand Meyer, a pioneer of object technology)
Software engineers want to be real engineers. Real engineers use mathematics. Formal methods are the mathematics of software
engineering. engineering
Therefore, software engineers should use formal methods.
(Mike Holloway, NASA) (Mike Holloway, NASA)
(cid:132) Major goal of software engineers
(cid:133) Develop reliable systems
(cid:132) Formal Methods
(cid:133) Mathematical languages, techniques and tools (cid:133) Used to specify and verify systems (cid:133) Goal: Help engineers construct more reliable systems
(cid:132) A mean to examine the entire state space of a
g g j
( h th ft
for all possible inputs for all possible inputs
design (whether hardware or software) d i ) h d (cid:133) Establish a correctness or safety property that is true
Past years of the formal methods (cid:132) Past years of the formal methods (cid:133)Obscure notation (cid:133)Non scalable techniques (cid:133)Non-scalable techniques (cid:133)Inadequate tool support (cid:133)Hard to use tools (cid:133)Hard to use tools (cid:133)Very few case studies (cid:133)Not convincing for practitioners (cid:133)Not convincing for practitioners
Nowadays (cid:132) Nowadays (cid:133)Trying to find more rigorous notations (cid:133)Model checking and theorem proving (cid:133)Model checking and theorem proving
(cid:133)More industrial sized case studies (cid:133)More industrial sized case studies (cid:133)Researchers try to gaining benefits of using
complement simulation in Hardware industry
(cid:133)…
formal methods
Formal methods can be applied at various (cid:132) Formal methods can be applied at various points through the development process (cid:133)Specification (cid:133)Specification (cid:133)Verification
(cid:132) Specification: Give a description of the (cid:132) Specification: Give a description of the
(cid:132) Verification: Prove or disprove the
th
di
P
ifi
t
l
Using a language with a mathematically (cid:132) Using a language with a mathematically defined syntax and semantics
(cid:132) System properties (cid:132) System properties
(cid:133)Functional behavior (cid:133)Timing behavior (cid:133)Timing behavior (cid:133)Performance characteristics (cid:133)Internal structure (cid:133)I t l
t t
(cid:132) Specification has been most successful for
p
(cid:132) A trend is to integrate different specification
behavioral properties
(cid:133) Performance (cid:133) Real-time constraints (cid:133) Security policies (cid:133) Architectural design (cid:133) Architectural design
languages (cid:133) Each enable to handle a different aspect of a system (cid:132) Some other non-behavioral aspects of a system
(cid:132) Formal methods for specification of the
t
sequential systems l ti (cid:133) Z (Spivey 1988) (cid:133) Constructive Z (Mirian 1997) (cid:133) Constructive Z (Mirian 1997) (cid:133) VDM (Jones 1986) (cid:133) Larch (Guttag & Horning 1993) (cid:133) Larch (Guttag & Horning 1993)
(cid:132) States are described in rich math structures ) (set, relation, function) ( (cid:132) Transition are described in terms of pre- and
, ,
p post- conditions
(cid:132) Formal methods for specification of the
T
p
(cid:132) States range over simple domains, like integers (cid:132) States range over simple domains like integers (cid:132) Behavior is defined in terms of sequences,
concurrent systems (cid:133) CSP (Hoare 1985) (cid:133) CCS (Milner 1980) (cid:133) Statecharts (Harel 1987) (cid:133) Temporal Logic (Pnueli 1981) li 1981) l L i (P (cid:133) I/O Automata (Lynch and Tuttle 1987)
trees, partial orders of events trees partial orders of events
Formal methods for handling both rich (cid:132) Formal methods for handling both rich state space and complexity due to concurrency concurrency (cid:133)RAISE (Nielsen 1989) (cid:133)LOTOS (ISO 1987) (cid:133)LOTOS (ISO 1987)
(cid:132) The CICS project (cid:132) CICS: Customer Information Control System
g y
p (cid:133) The on-line transaction processing system of choice for large IBM installations
(cid:132) In the 1980s Oxford Univ. and IBM Hursley Labs
p j
(cid:132) There was an overall improvement in the quality
formalized parts of CICS with Z f f CICS i h Z li d
(cid:132) It is estimated that it reduced 9% of the total
of the product d t f th
development cost development cost
This work won the Queen s Award for (cid:132) This work won the Queen’s Award for Technological (cid:133)The highest honor that can be bestowed on a (cid:133)The highest honor that can be bestowed on a
UK company.
(cid:132) CUTE: A Concolic Unit Testing g
(cid:132) Developed by a team managed by
Engine for C
(cid:133) use the symbolic execution to generate inputs that direct a program to alternate paths paths
(cid:133) use the concrete execution to guide
the symbolic execution along a concrete path
Gul Agha – 2005 (cid:132) Concolic testing
(cid:132) CUTE took less than 2 seconds to find two
previously unknown errors! previously unknown errors! (cid:133)a segmentation fault (cid:133)an infinite loop (cid:133)an infinite loop
(cid:132) The homepage of CUTE:
(cid:133)http://osl.cs.uiuc.edu/~ksen/cute/
http://www.cse.ogi.edu/S3S/JohnHarrison.pdf
(cid:133) Verification of Intel Pentium 4 floating-point unit with a
mixture of STE and theorem proving
(cid:133) Verification of bus protocols using pure temporal logic
model checking
(cid:133) Verification of microcode and software for many Intel (cid:133) Verification of microcode and software for many Intel Itanium floating-point operations, using pure theorem proving
(cid:132) FV found many high-quality bugs in P4 and
y (cid:132) Intel uses formal verification quite extensively q
(cid:132) FV is now standard practice in the floating-point
verified “20%” of design
domain
(cid:132) Small Aircraft Transportation System (SATS)
http://sats.nasa.gov/
(cid:132) Use of a software system that will sequence t
f ft th t ill
(cid:132) There are serious safety issues associated with these software systems and their underlying key these software systems and their underlying key algorithms
U aircraft into the SATS airspace in the absence of an airport controller an airport controller
The criticality of such software systems (cid:132) The criticality of such software systems necessitates that strong guarantees of the safety be developed for them safety be developed for them
(cid:132) Under the SATS program NASA Langley researchers are currently investigating researchers are currently investigating rigorous verification of these software system using formal methods system using formal methods (cid:133)Modeling and Verification of Air Traffic (cid:133)Conflict Detection and Alerting (cid:133)Conflict Detection and Alerting (cid:133)…
Two well established approaches to (cid:132) Two well established approaches to verification (cid:133)Model Checking (cid:133)Model Checking (cid:133)Theorem Proving
(cid:132) Model checking (cid:132) Model checking
(cid:133)Build a finite model of system and perform an
(cid:133)Mechanization of a logical proof f
exhaustive search exhaustive search (cid:132) Theorem Proving f M h ti l i l i
The technical challenge is to devise an (cid:132) The technical challenge is to devise an algorithm for handling large spaces (cid:132) Rebeca uses compositional verification (cid:132) Rebeca uses compositional verification
There are two general approaches in (cid:132) There are two general approaches in model checking 1. Temporal Model Checking 1 Temporal Model Checking 2. Model checking with a automaton spec
(cid:132) The difference is between the (cid:132) The difference is between the
specification (cid:133) First one : Temporal Logic (cid:133) First one : Temporal Logic (cid:133) Second one : Automaton
(cid:132) Model checking is completely automatic (cid:132) It produces counter examples
(cid:133) The counter example usually represents subtle error in design t t Th
(cid:132) The main disadvantage : state explosion problem! !
i di d
bl
t
l
i
(cid:132) Several approaches for facing the state
pp g
El
S
ti
ti
i
i
(cid:132) Checking large systems by using appropriate
explosion (cid:133) Ordered binary decision diagrams (BDD) – McMillan (cid:133) Partial Order – Peled (cid:133) Localization reduction – Kurshan (cid:133) Semantic minimization – Elseaidy id i
abstraction techniques abstraction techniques (cid:133) Burch et al. 10 ^ 120 states!
(cid:132) Both the system and its desired properties are
p p y
(cid:132) Theorem proving is the process of finding a
expressed in some mathematical logic
(cid:132) It can be roughly classified (cid:133) Highly automated programs (cid:133) Interactive systems with special purpose capabilities (cid:132) In contrast to model checking, it can deal with
proof from the axioms of the system
(cid:132) Relies on techniques like reduction
infinite space R li t h i d ti lik
Pham Ngoc Hung, Coltech, VNU, 2009
29
