SWEN90010 – High Integrity
Systems Engineering Checking Formal Specifications
Toby MD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
Copyright By PowCoder代写 加微信 powcoder
Alloy Modelling Overview
signatures: declaring sets and relations
facts: axioms that hold over signatures and globally constrain the model to rule out nonsense
predicates: define relations between variables in a model, used to specify operations, state transitions
functions: shorthand for expressions
2 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Finite State Machines
Begin in an initial state s0
States are just collections of variables of different types. Have a collection of operations that each alter the state.
Each operation implements a different state transition.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Modelling FSMs in Alloy
States are collections of (typed) variables: sig State {…}
Possibly constrained using:
fact blah { always all s : State | … }
Initial state: pred Init[s : State] { … } Operations: pred Op1[s : State] { … } pred Opn[s : State] { … }
Predicates might make use of functions fun as shorthands 4 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Finite State Machines
Begin in an initial state s0
States are just collections of variables of different types. Have a collection of operations that each alter the state.
Each operation implements a different state transition.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
CHECKING SPECIFICATIONS IN ALLOY
“Formal verification is able to tell that a program was built right, but it cannot tell that the right program was built.”
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Checking a Specification
How do we know that our specification has correctly captured our intentions?
(“run” the spec to see what behaviours it captures)
Check Assertions
(see what properties might follow from the spec)
Alloy’s run command
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Finds instances that satisfy predicates within a specified bound
(begin with smallest reasonable bound, increase it if unsatisfiable)
Alloy’s assert statement
Declare properties that should follow from the specification.
9 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Alloy’s check command
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Searches up to a fixed bound for counterexamples that violate a property.
(use “expect” to annotate which checks should pass and which should fail)
(begin with smallest reasonable bound, increase it if no counterexample found)
DeleteIsUndo Example
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Invalid Counterexamples
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Like testing an assertion for all systems up to the bound
Doesn’t prove the assertion will hold for systems of arbitrary size in general
Although it might for specific systems and assertions.
In general, it gives very high confidence if not a proof. Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Assertions as Tests
Alloy does bounded assertion checking
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Assertion Confidence
If Alloy says the assertions all hold, is my spec right?
Checks only within finite bounds. Spec could be incomplete.
Spec could say the wrong thing.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com