SWEN90010 – High Integrity
Systems Engineering Formal Verification and Validation
Toby MD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
Copyright By PowCoder代写 加微信 powcoder
Specification Process
2 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
State Invariants
How to check a predicate Inv[s] of all states s in a state machine?
assert invInit { all s : State | Init[s] => Inv[s] }
assert invOpi { always all s : State | Inv[s] and Opi[s] => after Inv[s] }
(for each operation opi)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Exceptional Behaviour
Distinguishing normal and exceptional behaviour in models
4 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Exceptional Behaviour
The point is to constrain what the system is meant to do in exceptional cases
5 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Exceptional Behaviour
Model it separately from normal behaviour Where does it come from?
e.g. Hazard Analysis (HAZOP) etc.
6 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
How are these two predicates different?
Second allows pb.password in the post-state to be anything, and so allows add¡¯s exceptional behaviour to be arbitrary
7 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
What does this spec say?
Imagine that Objs have two variable fields, x and y
pred addToX [o : Obj] { o.x¡¯ = o.x + …
Allows the y field to change arbitrarily. It should be:
pred addToX [o : Obj] { o.x¡¯ = o.x + …
o.y¡¯ = o.y
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
V&V FOR SPECS
V&V for formal specs
How do we do V&V for our specs?
Animation (e.g. Alloy¡¯s run command) Model Checking (e.g. Alloy¡¯s check command) Implement and test
Reviews and Inspections
10 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
add[pb, user, url, pwd, res] = addNormal[pb, user, url, pwd, res] or addExceptional[pb, user, url, res]
all pb, user, url, pwd, res |
Inv[pb] and add[pb,user,url,pwd,res] =>
after Inv[pb]
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
all pb, user, url, pwd, res |
Inv[pb] and
(addNormal[pb, user, url, pwd, res] or
addExceptional[pb, user, url, res]) => after Inv[pb]
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
all pb, user, url, pwd, res |
(Inv[pb] and addNormal[pb, user, url, pwd, res]) or
(Inv[pb] and addExceptional[pb, user, url, res]) =>
after Inv[pb]
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
Consider both cases of the or
all pb, user, url, pwd, res |
Inv[pb] and addNormal[pb, user, url, pwd, res]) =>
after Inv[pb]
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
addNormal[pb, user, url pwd, res] =
no pb.password[user][url]
pb.password¡¯ = pb.password + (user->url->pwd) res in Success
addNormal[pb, user, url pwd, res] =
no pb.password[user][url]
pb.password¡¯ = pb.password + (user->url->pwd) res in Success
all pb, user, url, pwd, res |
Inv[pb] and no pb.password[user][url] and pb.password¡¯ = pb.password + (user->url->pwd) =>
after Inv[pb]
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
all pb, user, url, pwd, res |
Inv[pb] and no pb.password[user][url] and pb.password¡¯ = pb.password + (user->url->pwd) =>
after Inv[pb]
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
Inv[pb] = all user, url | lone pb.password[user][url]
all pb, user, url, pwd, res |
(all user1, url1 | lone pb.password[user1][url1]) and no pb.password[user][url] and
pb.password¡¯ = pb.password + (user->url->pwd) =>
(all user2, url2 | lone pb.password¡¯[user2][url2]) Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
Two cases to consider: user2, url2 are user, url or not
all pb, user, url, pwd, res |
(all user1, url1 | lone pb.password[user1][url1]) and no pb.password[user][url] and
pb.password¡¯ = pb.password + (user->url->pwd) =>
(lone pb.password¡¯[user][url])
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
user2, url2 are user, url
all pb, user, url, pwd, res |
(all user1, url1 | lone pb.password[user1][url1]) and no pb.password[user][url] and
pb.password¡¯ = pb.password + (user->url->pwd) =>
(all user2, url2 | lone pb.password¡¯[user2][url2]) Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof: An Example
user2, url2 are not user, url
Proof: An Example
all pb, user, url, pwd, res |
Inv[pb] and addExceptional[pb, user, url, pwd, res]) =>
after Inv[pb]
20 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
This kind of reasoning can be somewhat automated
Proof Assistants (Theorem Provers), e.g.: Isabelle, Coq, HOL4 etc.
Automated Provers: e.g. SAT, SMT solvers etc. (e.g. MiniSAT, Z3)
Can also be applied to code. (See later in the course.)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Model Checking
Automatically check that every state of a (finite sized) system satisfies some property.
Give a counterexample when the check doesn¡¯t hold: a state for which the property is false.
Successes:
Hardware Verification Security Protocol Verification
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com