程序代写 SWEN90010 – High Integrity

SWEN90010 – High Integrity
Systems Engineering Logic Intro

Copyright By PowCoder代写 加微信 powcoder

DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray

Story so far
Safety Engineering
Understanding them: HAZOP
Assess their possibility: FTA etc.
Formal Model-Based Specification (Formal) Model-Based Specification
(c.f. UML, Statecharts)
2 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Requirements Design

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Logical Specifications
First we need a logic
This course: (first order) set theory / predicate logic
Then, we want a mechanised way to reason in the logic (i.e. prove things about our specs)
This course: Alloy

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Refresher / Introduction to logic
Propositions Sets Predicates
Plus Alloy’s flavour of these.
see the LMS link on introductory
predicate logic and set theory if this stuff is new to you

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Propositions
A statement that is either true or false
atom “it is raining in Parkville” Raining(Parkville)
“it is raining” Raining
“it is raining in Parkville and it is not raining in Sydney”
compound proposition

Propositional Connectives
Traditional Notation
Raining(Parkville) implies not Raining(Sydney) Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
and or not implies
Raining(Parkville) and not Raining(Sydney)

Variables allow propositions to talk about state
averageVelocity > 10
averageVelocity > 10 and currentVelocity = 11 Variables talk about different parts of the state of
the formal model. (not state of the system/program) Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

universe empty set
union intersection
difference
A collection of things
“the set containing 3 and 5”
“the set of even numbers” the set holding everything the set of nothing
everything in A and everything in B everything that’s in both A and B
everything in B that is not in A
{ x | even(x) } univ none
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Set Operations
9 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Set Operations
Union: A + B
10 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Set Operations
Intersection: A & B
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Set Operations
Difference: A – B
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Set Relationships
Disjoint: no A & B
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Set Relationships
Subset: A in B
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

singleton cardinality
x is a member of set A everything in B is also in A
“the set holding just the number 3” the number of things in set A
set A is empty
in Alloy, everything is a set, even single elements
x in A B in A 3 #A no A
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Predicates
Extend propositions with the ability to quantify the values of a variable that a proposition is true for
all: Proposition P(x) holds for all values of x all x | P(x)
all city | Raining(city)
all city : AustralianCities | Raining(city)
some: Proposition P(x) holds for at least one value of x
some x | P(x)
some city | not Raining(city)

Quantification
De Morgan’s Laws
all x | P(x) some x | P(x)
one x | P(x) lone x | P(x) none x | P(x)
is equivalent to not some x | not P(x) is equivalent to not all x | not P(x)
Alloy Specific Quantifiers
P(x) holds for exactly one value x P(x) holds for at most one value x
P(x) holds for no value x
17 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
A proposition that relates things together =, <, etc. arity: the number of things the relation relates =, < etc. are all binary relations; relate two numbers 3 < 4, (5 - 1) = (3 + 1), etc. A relation that relates three things together: IsSum(x,y,z) ⇔ z = x + y Relations are just predicates What Is A Relation? How would you write down unambiguously what a relation means? Simplest answer: just list all of the things it relates together. Sum(x,y,z) 120 -5 115 ... Each row is a tuple: (x, y, z) Any relation is a simply a set of tuples. Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Relations as Sets Factor(x,y,z) — when y and z are factors of x Each row is a tuple: (x, y, z) Any relation is a simply a set of tuples. Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Relations as Sets Factor(x,y,z) — {(x,y,z) | x = y * z} {(1,1,1), (2,1,2), (2,2,1), (3,1,3), (3,3,1),(4,4,1), (4,2,2),...} Use Factor to define when a number is prime, i.e. define the predicate IsPrime(x) all y,z | (x,y,z) in Factor implies y = 1 or z = 1 Relations as Sets A relation with arity n (i.e. an n-ary relation) R, is a set of n-tuples of atoms. A binary (2-ary) relation R(a,b) is a set of: pairs A ternary (3-ary) relation R(a,b,c) is a set of: triples A unary (1-ary) relation R(a) is a set of: atoms i.e. just an ordinary set Sets are relations, and relations are sets. Sets are predicates, and predicates are sets. Relations are predicates, and predicates are relations. 22 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Binary Relations as Pictures Less Than: < Domain Range 23 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Relation Example Imagine 2 sets of atoms: Username = {n1, n2, ...} Password = {p1, p2, ...} Imagine an LDAP username/password database. LDAPDB : Username -> Password
LDAPDB ⊆ 𝒫 (Username x Password)
24 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Every username has only one password
25 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

For every username, there is only one password in LDAPDB
all u:Username, pw1:Password, pw2:Password | LDAPDB(u,pw1) and LDAPDB(u,pw2) implies pw1 = pw2
LDAPDB is a function
26 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Total vs Partial Functions
LDAPDB : Username -> Password
Does every username in Username have a password?
A total function gives an answer for every (type-correct) argument
A partial function is one that is not total. Domain
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
domain(LDAPDB)
28 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
range(LDAPDB)
29 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
LDAPDB + (u4 -> p2)
u2 p2 u3 p3
30 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
LDAPDB + (u4 -> p2)
u2 p2 u3 p3
31 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
LDAPDB ++ (u3 -> p2)
u2 p2 u3 p3
32 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
LDAPDB ++ (u3 -> p2)
u2 p2 u3 p3
33 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
{u1,u2} <: LDAPDB u2 p2 u3 p3 34 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Relation Operations {u1,u2} <: LDAPDB u2 p2 u3 p3 35 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License Relation Operations LDAPDB :> {p1,p3}
u2 p2 u3 p3
36 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Operations
LDAPDB :> {p1,p3}
37 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Joins
Consider two relations (as sets)
(0,1) (1,1,1) (1,2) (2,2,1) (2,3) (2,1,2)
(3,1,3) (3,3,1) (4,4,1) (4,1,4) (4,2,2)
38 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Joins
Consider two relations (as sets)
(0,1) (1,1,1) (1,2) (2,2,1) (2,3) (2,1,2)
(3,1,3) (3,3,1) (4,4,1) (4,1,4) (4,2,2)
39 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Joins
Consider two relations (as sets)
(0,1) (1,1,1) (1,2) (2,2,1) (2,3) (2,1,2)
(0,1,1) (1,2,1) (1,1,2)
(3,1,3) (2,1,3) (3,3,1) (2,3,1) (4,4,1) (3,4,1) (4,1,4) (3,1,4) (4,2,2) (3,2,2)
40 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Relation Joins
(0,1) (1,1,1) (1,2) (2,2,1) (2,3) (2,1,2)
(0,1,1) (1,2,1) (1,1,2)
(3,1,3) (2,1,3) (3,3,1) (2,3,1) (4,4,1) (3,4,1) (4,1,4) (3,1,4) (4,2,2) (3,2,2)
41 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Where Next?
How to use this to model in software engineering.
Why do that? Advantages and disadvantages.
How to do this in Alloy and show properties of models.
42 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com