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