deck_15620570 Flashcards
(41 cards)
What is denotational semantics?
a method used to formally define the meaning of programming constructs by mapping them to mathematical objects
focuses on what a program means rather than how it is executed, providing a precise understanding of its behavior using mathematical structures like sets and functions
What is partial correctness?
addresses whether a program, when it terminates, reaches the correct state according to a specified specification
verifies if the program produces the desired output when it halts, assuming it does indeed terminate
“partial” because it doesn’t consider whether the program will always terminate (which is covered by total correctness), but only concerns itself with correctness upon termination
Three principles of the Classical View of Programs?
- Denotational semantics
- Partial correctness
- Nontermination is bad
What is a reactive system?
a system that responds to stimuli from its environment
focuses on communication and interaction
often parallel
nontermination is good
e.g., operating systems, mobile phones, vending machines
What are the two views on reactive systems?
- A process performs an action and becomes another process (Labelled Transition Systems)
- A process changes state and becomes another process (Kripke Structure)
What is a Kripke Structure? Formal definition
A tuple (S, s0, ->, AP, L) where:
S is a set of states
s0 is the initial state
-> (subset of S * S) is a total transition relation
AP is a set of atomic propositions
L:S -> 2^(AP) is a labelling function that assigns a set of atomic propositions to every state
What is a Kripke Structure? Informal definition
A graph representing the behaviour of the system, where:
The nodes (circles) represent reachable states.
The edges (arrows) represent transitions between state.
The labelling function maps aech state to a set of properties that hold in that state.
What is a path “pi” in a Kripke structure?
A path pi starting in state s is a sequence of states pi = s,s1,s2,s3,s4,… such that s->s1 and si-1 -> si for all i>0
“pi”[i] represents the state at position i in the path pi
“pi”[i…] represents the suffix of the path pi starting at position i
What is PROMELA?
A programming language that can be used to model Kripke structures
Main Components of a PROMELA Model
- Type declarations
- Channel declarations
- Variable declarations
- Process declarations
- “init” process
Data Types in PROMELA
- Five Basic types:
- bit (0/1)
- bool (false/true)
- byte (0, 255)
- short(many more integers)
- int (even more integers) - Arrays:
- e.g., byte a[27] or bit flags[4] - Records:
- e.g.,:
typedef Rectangle {
int width;
int height;
}
Rectangle rr;
rr.width = …
- Message Types/ Enumerations:
- e.g.,:
mtype:fruit = {apple, pear};
mtype:size = {small, medium};
Defining a process body in PROMELA
e.g.,:
proctype Name(int parameter) {
x = 1; //assignment
skip; // no action
int y = 1; // assignment
x < 2 && y == 1; // code waits here until this is satisfied
}
Executability of Statements in PROMELA:
A statement is either executable or it is blocked.
if the process arrives at a blocked statement, it will stop
statements like skip, assignments, declarations, printf are always executable
an expression is executable if it evaluates to true (or a non zero value)
Non-deterministic choice in PROMELA
if statements where multiple if branches are true
if none are true, if-statement blocks
e.g.,
if
:: (true) -> skip;
:: (false) -> skip:
:: else -> skip;
fi
Loops in PROMELA
Use do-statements
very similar to if-statement as it needs conditions and any of the true branches may be taken
however once this is finished, the loop returns to the beginning
break statements can be used to transfer control to the end of the do-statement
do
:: (true) -> skip;
:: (false) -> skip;
else -> skip;
od
How can one instantiate a process in PROMELA?
Processes can be instantiated by using the run keyword.
E.g., for process bruh, run(bruh) instantiates this process
When are run statements blocked?
when 255 procesess are already running
What does the keyword active mean for processes? What does active[N] proctype bruh mean?
Means that the process is instantiated from the start.
Means that N instances of the process are instantiated from the start.
How is control flow passed in between processes in PROMELA?
all processes are executed concurrently, independently of the speed of the behaviour
How do processes communicate in between each other in PROMELA?
through global variables and channels
Global variables in PROMELA
defined at the top-level
can be read and updated just like local variables
Atomic Statements in PROMELA
can be used to group together statements into an atomic sequences
all statements in such a sequence are thus executed in a single step, i.e., with no interleaving with statements of other processes
statement is executable if stat1 is executable, where stat1 is the first action in the sequence
if any process inside the sequence is blocked, the atomicity token is lost and other processes can execute a step
can be used to reduce the nr of states of a model
Types of Properties Able to be Checked By Spin
- Deadlocks
- Unreachable code
- Assertions
- Linear Time Logic (LTL) Formulas
What are deadlocks in PROMELA?
bad endstates, or situations in a concurrent system where two or more processes are unable to proceed because each is waiting for the other to release a resource, leading to a standstill
