SWEN90010 – High Integrity
Systems Engineering Formal Specification
Copyright By PowCoder代写 加微信 powcoder
DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
TEMPORAL LOGIC (TALKING ABOUT TIME)
Next State
if x is a variable, then x’ refers to x’s value
in the next state
To specify that x is incremented, we would write
x’ = x + 1
Predicates that talk about x are also allowed to talk about x’s value in future states, e.g. x’, x’’ etc. and how it relates to x’s current value
These predicates define state transitions Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Transitions and Traces
x’ = x + 1
If in s1, x = 5, then in s2, x = 6
A sequence of transition is called a trace
4 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Temporal Operators
We can also write predicates that talk about future and even past states using temporal operators
assuming the current state is s0
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Temporal Operators
We can also write predicates that talk about future and even past states using temporal operators
assuming the current state is s0
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Temporal Operators
We can also write predicates that talk about future and even past states using temporal operators
eventually P
P holds in at least one of these states assuming the current state is s0
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Temporal Operators
We can also write predicates that talk about future and even past states using temporal operators
equivalent to P and (after Q)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Temporal Operators
We can also write predicates that talk about future and even past states using temporal operators
We will meet others in this subject. See course notes for more information
SPECIFICATIONS SAY “WHAT” DESIGNS SAY “HOW”
Specifying Software
Specify modules
Formally describe (an abstraction of) the module’s state
Formally describe the behaviour of the module’s operations (e.g. procedures, functions etc.).
Behaviour specified in terms of state (transition) relations.
natural number
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Trivial example: a counter
Operation:
Aside: Functions as Relations
Suppose we have a function f : A → B f is just a relation
i.e. a set of pairs: (a,b)
(ai) (a1,b1)
(a2,b2) (a3,b3)
(ai,bi) …
Consider some ai : A What is f[ai] ?
What is ai?
f[ai] is equivalent to ai.f
which is {(bi)}
i.e. f[ai] = bi
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Modelling Data Types
Data types modelled as sets, relations, functions etc.
Example: a sequence (e.g. list, array, etc.) of Ts
A function: Z+ → T i.e. a set of pairs: (index,t)
Sequence Operations: for a sequence seq
seq(i) length(seq)
append(seq,el)
seq[i] #seq
seq ++ ((#seq +1) -> el)
Sequences as Relations
For a sequence seq : Z+ → T
domain(seq)
range(seq) seq :> t
#(seq :> t)
valid list indices, i.e. {1..#seq}
set of elements in the list
{(index,e) : seq | e = t}
number of occurrences of t
index element
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Example: Searching
Searching a sorted list (e.g. binary search)
— returns -1 if target doesn’t exist in list
— assumes the list is sorted
procedure Search(list : in ElementList; target : in Element;
index : out Integer);
Suppose we call Search(list,t,index) What relationship should hold now between
Should this hold for all lists?
list, t and index? list[index] = t
index = -1 and t not in range(list)
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Pre and Postconditions
Precondition: Specifies the assumptions made by a procedure/function
Postcondition: Specifies the behaviour, assuming that the precondition holds
Precondition for binary search: list is sorted
sorted(list) ⇔ all i : Z | i < #list implies list[i] ≤ list[i+1]
Example: Searching again
Searching a sorted list (e.g. binary search)
-- returns -1 if target doesn’t exist in list
-- assumes the list is sorted
procedure Search(list : in ElementList; target : in Element;
index : out Integer);
Suppose we call Search(list,t,index) What relationship should hold now between
list, t and index?
postcondition
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
sorted(list) and precondition
list[index] = t
index = -1 and t not in range(list)
Model the behaviour of each operation as a relation The relation captures the relationship between the
operation’s inputs and outputs
In general:
relates the states before and after the operation
Says how they are allowed to differ (postcondition) under assumptions about the inputs (precondition)
Says what the operation does, not how it does it. Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Formal Model-Based Specs
Advantages
Unambiguous
Abstract from Implementation
Machine-Checkable
Forces thinking up-front
Gets mistakes out of the way early (i.e. when they are cheaper to fix)
19 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Effect on Cost
20 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Z not used
Problems per 1KLOC
Product level design
Component level design
Module level design
Functional
verification
System test
Effect on Cost
formal specification not necessarily more expensive overall
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Disadvantages
Requires specialised expertise
Might lengthen time to implementation Loads more effort early in the development process
Not necessarily well suited to projects with rapidly changing requirements.
(So it’s important to get your HAZOP etc. correct)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Difficulty
All programmers know many formal languages
Specs are shorter and thus simpler to write than code
Specs say only what not how
Programs must say both
Ordinary programmers not trained to write and read formal specs
SPECIFICATIONS IN ALLOY
Alloy all x : S | ...
open package/m2 ...
Logic + Language + Tool
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
LASTPASS DEMO
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
27 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com