107 -> 1020 states and more
A Brief History of FV
Late 80s and early 90s:
Deal with state explosion OBDD Abstraction Modularity Symmetry
A Brief History of FV
Verification:Are we building the prodict right? Validation:Are we building the right prodict?
Simulation vs. Emulation vs.Test
Simulation(模拟 performed on the model 模拟): 模拟 Emulation(仿真 performed on prototyping 仿真): 仿真 Test(测试 performed on the actual product 测试): 测试 (manufacturing test)
Safety critical systems Commercially critical systems Mission critical systems
What is verification?
Theoretically, verification means proof of correctness
Verification vs Validation
Verification: is the procees checking if the product is built correctly according to the specification. Validation: is the procees that ensures that the product meets the expectation of the user. In Boehm word:
Small tricky(技巧的) programs manually annotated and proved
A Brief History of FV
1970s: Progress in automated deduction related to program verification
1973: [Boyer Moore] Computational Lisp 1975: [Nelson Oppen] Decision procedures for combination logic theories 1976: [D Gordon ] Higher Order Logic theorem proving (LCF) 1977: [F Pnueli] introduces (linear) temporal logics(LTL) as a formalism to reason about reactive systems
Chapter 5 Formal Verification
5.1 Overview 5.2 Theorem proving 5.3 Model Checking
5.1 Overview
What is Verification? What is formal Verification Formal Verification Methods Formal Verification Process A Brief History of FV
What is formal Verification?
Formal verification means to apply mathematical arguments to prove the correctness of systems Formal means two things:
A mathematical (not English) specification An exhaustive(彻底的) verification method (not simulation)
Automatic: Model Checking Semi-automatic (deductive/theorem proving)
Practically, it mainly attempts to increase reliability:
Automated systematic debugging VERY good at finding errors!
Formal Verification Process
1. Modelling
What the system actually does Expressed as a set of predicates, or as an automaton
2.
What the system ought to do Expressed in an assertion language, e.g., boolean logic,LTL,CTL,µ-calculus,…
A Brief History of FV
1960s: [Floyd,McCarthy] Program verification
Partial vs total correctness
1970s: [Hoare, Dijkstra] Logics for programs, axiomatic semantics (connect programs to logic), logical transformations for program constructs
Determine
Can we construct a proof for S (from A) in calculus C?
What is Theorem Proving?
Logic = Syntax + Semantics + Calculus TP = Proof-search in C (Huge search problem) Correctness and completeness of Calculi are essential properties Calculus = Non-deterministic Algorithm Central problem in TP: How to implement a non-deterministic algorithm efficiently on a deterministic machine
“State Explosion”Problem
Formal Verification Process
Formal Verification process consist of three parts:
1.A framework for Formal modeling systems some kind of modeling language 2.A Formal specification language for describing the properties to be verified 3.A Formal verification method for establishing if the description of the system satisfies the specification
Formal Verification Methods
Deductive演绎verification
Automated theorem proving
Interactive verification
Semi-automated theorem proving Formal Verification
What is Verification?
Verification: verifying the correctness of products
Hardware, software, embedded control systems, network protocols, …
It is most obvious in
a formal language (or logic) L a calculus C for this language (= set of rules) a conjecture (猜想)S and a set of assumptions or axioms A in the language L
By 1990s: Basic theoretical problems worked out 1990s: Emphasis on infinite state systems
Real time systems (timed automata) Embedded systems (hybrid automata) Models with stacks, queues, …(ADT)
Difficult and time consuming
for critical applications only
Formal Verification Methods
Interactive verification Analysis reduces to proving a theorem in a logic Uses interactive theorem prover(ITP) Requires more expertise
A Brief History of FV
1981: [Clarke, Emerson and Quielle Sifakis] independently discover finite state temporal logic model checking
Applied to digital circuits