CS 228 : Logic in Computer Science
Krishna. S
1/23
Some Real Life Stories
2/23
Therac-25(1987)
◮ The Therac-25 : radiation therapy machine produced by Atomic
Energy of Canada Limited (AECL)
3/23
Therac-25(1987)
◮ The Therac-25 : radiation therapy machine produced by Atomic
Energy of Canada Limited (AECL)
◮ Involved in at least six accidents, in which patients were given
massive overdoses of radiation, approximately 100 times the
intended dose.
3/23
Therac-25(1987)
◮ The Therac-25 : radiation therapy machine produced by Atomic
Energy of Canada Limited (AECL)
◮ Involved in at least six accidents, in which patients were given
massive overdoses of radiation, approximately 100 times the
intended dose.
◮ Design error in the control software (race condition)
3/23
Intel Pentium Bug (1994)
◮ The Intel FDIV bug : Bug in the intel P5 floating point unit
4/23
Intel Pentium Bug (1994)
◮ The Intel FDIV bug : Bug in the intel P5 floating point unit
◮ Discovered by a professor working on Brun’s constant
◮ ( 31 + 51 ) + ( 15 + 17 ) + ( 11
1
+ 1
13 )
1
+ ( 17 + 1
19 ) + . . . converges to
∼
B = 1.90216054
4/23
Intel Pentium Bug (1994)
◮ The Intel FDIV bug : Bug in the intel P5 floating point unit
◮ Discovered by a professor working on Brun’s constant
◮ ( 31 + 51 ) + ( 15 + 17 ) + ( 11
1
+ 1
13 )
1
+ ( 17 + 1
19 ) + . . . converges to
∼
B = 1.90216054
◮ Intel offered to replace all flawed processors
4/23
Ariane 5 (1996)
◮ ESA (European Space Agency) Ariane 5 Launcher
5/23
Ariane 5 (1996)
◮ ESA (European Space Agency) Ariane 5 Launcher
◮ Shown here in maiden flight on 4th June 1996
5/23
Ariane 5 (1996)
◮ ESA (European Space Agency) Ariane 5 Launcher
◮ Shown here in maiden flight on 4th June 1996
◮ Self destructs 37 secs later
5/23
Ariane 5 (1996)
◮ ESA (European Space Agency) Ariane 5 Launcher
◮ Shown here in maiden flight on 4th June 1996
◮ Self destructs 37 secs later
◮ uncaught exception: data conversion from 64-bit float to 16-bit
signed int
5/23
Toyota Prius (2010)
◮ First mass produced hybrid vehicle
6/23
Toyota Prius (2010)
◮ First mass produced hybrid vehicle
◮ software “glitch” found in anti-lock braking system
◮ Eventually fixed via software update in total 185,000 cars recalled,
at huge cost
6/23
Nest Thermostat (2016)
◮ Nest Thermostat, the smart, learning thermostat from Nest Labs
7/23
Nest Thermostat (2016)
◮ Nest Thermostat, the smart, learning thermostat from Nest Labs
◮ software “glitch” led several homes to a frozen state, reported in
NY times, Jan 13, 2016. May be, old fashioned mechanical
thermostats better!
7/23
What do these stories have in
common?
◮ Programmable computing devices
◮ conventional computers and networks
◮ software embedded in devices
8/23
What do these stories have in
common?
◮ Programmable computing devices
◮ conventional computers and networks
◮ software embedded in devices
◮ Programming error direct cause of failure
◮ Software critical
◮ for safety
◮ for business
◮ for performance
8/23
What do these stories have in
common?
◮ Programmable computing devices
◮ conventional computers and networks
◮ software embedded in devices
◮ Programming error direct cause of failure
◮ Software critical
◮ for safety
◮ for business
◮ for performance
◮ High costs incurred: financial, loss of life
◮ Failures avoidable
8/23
Formal Methods
Intuitive Description
“Applied Mathematics for modelling and analysing ICT systems”
Formal methods offer a large potential for:
9/23
Formal Methods
Intuitive Description
“Applied Mathematics for modelling and analysing ICT systems”
Formal methods offer a large potential for:
◮ obtaining an early integration of verification in the design process
9/23
Formal Methods
Intuitive Description
“Applied Mathematics for modelling and analysing ICT systems”
Formal methods offer a large potential for:
◮ obtaining an early integration of verification in the design process
◮ providing more effective verification techniques (higher coverage)
9/23
Formal Methods
Intuitive Description
“Applied Mathematics for modelling and analysing ICT systems”
Formal methods offer a large potential for:
◮ obtaining an early integration of verification in the design process
◮ providing more effective verification techniques (higher coverage)
◮ reducing the verification time
9/23
Simulation and Testing
Basic procedure
◮ Take a model
◮ Simulate it with certain inputs
◮ Observe what happens, and if this is desired
Important Drawbacks
◮ possible behaviours very large/infinite
◮ unexplored behaviours may contain fatal bug
◮ can show presence of errors, not their absence
10/23
Model Checking
◮ Year 2008 : ACM confers the Turing Award to the pioneers of
Model Checking: Ed Clarke, Allen Emerson, and Joseph Sifakis
◮ Why?
11/23
Model checking
◮ Model checking has evolved in last 25 years into a widely used
verification and debugging technique for software and hardware.
◮ Cost of not doing formal verification is high!
◮ The France Telecom example
◮ Ariane rocket: kaboom due to integer overflow!
◮ Toyota/Ford recalls
12/23
Model checking
◮ Model checking has evolved in last 25 years into a widely used
verification and debugging technique for software and hardware.
◮ Cost of not doing formal verification is high!
◮ The France Telecom example
◮ Ariane rocket: kaboom due to integer overflow!
◮ Toyota/Ford recalls
◮ Model checking used (and further developed) by
companies/institutes such as IBM, Intel, NASA, Cadence,
Microsoft, and Siemens, and has culminated in many freely
downloadable software tools that allow automated verification.
12/23
What is Model Checking?
System specification
satisfy?
good/bad properties
13/23
What is Model Checking?
System specification
satisfy?
model-checking
System Model Spec Model
|=?
13/23
Model Checker as a Black Box
◮ Inputs to Model checker : A finite state system M, and a property
P to be checked.
◮ Question : Does M satisfy P?
◮ Possible Outputs
◮ Yes, M satisfies P
◮ No, here is a counter example!.
14/23
What are Models?
Transition Systems
◮ States labeled with propositions
◮ Transition relation between states
◮ Action-labeled transitions to facilitate composition
15/23
What are Models?
Transition Systems
◮ States labeled with propositions
◮ Transition relation between states
◮ Action-labeled transitions to facilitate composition
Expressivity
◮ Programs are transition systems
◮ Multi-threading programs are transition systems
◮ Communicating processes are transition systems
◮ Hardware circuits are transition systems
◮ What else?
15/23
What are Properties?
Example properties
◮ Can the system reach a deadlock?
◮ Can two processes ever be together in a critical section?
◮ On termination, does a program provide correct output?
16/23
What are Properties?
Example properties
◮ Can the system reach a deadlock?
◮ Can two processes ever be together in a critical section?
◮ On termination, does a program provide correct output?
Logics of Relevance
◮ Classical Logics
◮ First Order Logic
◮ Monadic Second Order Logic
◮ Temporal Logics
◮ Propositional Logic, enriched with modal operators such as 2
(always) and 3 (eventually)
◮ Interpreted over state sequences (linear)
◮ Or over infinite trees (branching)
16/23
Two Traffic Lights
1. The traffic lights are never green simultaneously
∀x(¬(green1 (x) ∧ green2 (x))) or 2(¬(green1 ∧ green2 ))
2. The first traffic light is infinitely often green
∀x∃y(x < y ∧ green1 (y)) or 23green1
3. Between every two occurrences of traffic light 1 becoming red,
traffic light 2 becomes red once.
17/23
The Model Checking Process
◮ Modeling Phase
◮ model the system under consideration
◮ as a first sanity check, perform some simulations
◮ formalise property to be checked
18/23
The Model Checking Process
◮ Modeling Phase
◮ model the system under consideration
◮ as a first sanity check, perform some simulations
◮ formalise property to be checked
◮ Running Phase
◮ run the model checker to check the validity of the property in the
model
18/23
The Model Checking Process
◮ Modeling Phase
◮ model the system under consideration
◮ as a first sanity check, perform some simulations
◮ formalise property to be checked
◮ Running Phase
◮ run the model checker to check the validity of the property in the
model
◮ Analysis Phase
◮ property satisfied? → check next property (if any)
◮ property violated? →
◮ analyse generated counter example by simulation
◮ refine the model, design, property, . . . and repeat entire procedure
◮ out of memory? → try to reduce the model and try again
18/23
The Pros of Model Checking
◮ widely applicable (hardware, software...)
◮ allows for partial verification (only relevant properties)
◮ potential “push-button” technology (tools)
◮ rapidly increasing industrial interest
◮ in case of property violation, a counter example is provided
◮ sound mathematical foundations
◮ not biased to the most possible scenarios (like testing)
19/23
The Cons of Model Checking
◮ model checking is only as “good” as the system model
◮ no guarantee about completeness of results (incomplete
specifications)
Neverthless:
Model Checking is an effective technique to expose potential design
errors
20/23
Striking Model-Checking Examples
◮ Security : Needham-Schroeder encryption protocol
◮ error that remained undiscovered for 17 years revealed (model
checker SAL)
◮ Transportation Systems
◮ Train model containing 1047 states (model checker UPPAAL)
◮ Model Checkers for C, JAVA, C++
◮ used (and developed) by Microsoft, Intel, NASA
◮ successful application area: device drivers (model checker SLAM)
◮ Dutch storm surge barrier in Nieuwe Waterweg
◮ Software in current/next generation of space missiles
◮ NASA’s
◮ Java Pathfinder, Deep Space Habitat, Lab for Reliable Software
21/23
Relevant Topics
◮ What are appropriate models?
◮ from programs, circuits, communication protocols to transition
systems
22/23
Relevant Topics
◮ What are appropriate models?
◮ from programs, circuits, communication protocols to transition
systems
◮ What are properties?
◮ Safety, Liveness, fairness
22/23
Relevant Topics
◮ What are appropriate models?
◮ from programs, circuits, communication protocols to transition
systems
◮ What are properties?
◮ Safety, Liveness, fairness
◮ How to check regular properties?
◮ finite state automata and regular safety properties
◮ Buchi automata and ω-regular properties
22/23
Relevant Topics
◮ How to express properties succintly?
◮ First Order Logic (FO) : syntax, semantics
◮ Monadic Second Order Logic (MSO) : syntax, semantics
◮ Linear-Temporal-Logic (LTL) : syntax, semantics
◮ What can be expressed in each logic?
◮ Satisfiability and Model checking : algorithms, complexity
23/23
Relevant Topics
◮ How to express properties succintly?
◮ First Order Logic (FO) : syntax, semantics
◮ Monadic Second Order Logic (MSO) : syntax, semantics
◮ Linear-Temporal-Logic (LTL) : syntax, semantics
◮ What can be expressed in each logic?
◮ Satisfiability and Model checking : algorithms, complexity
◮ How to make models succint?
◮ Equivalences and partial-orders on transition systems
◮ Which properties are preserved?
◮ Minimization algorithms
23/23
