CS代写 SWEN90010 – High Integrity

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