deck_15620570 Flashcards

1
Q

What is denotational semantics?

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

What is partial correctness?

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

Three principles of the Classical View of Programs?

A
  1. Denotational semantics
  2. Partial correctness
  3. Nontermination is bad
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

What is a reactive system?

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

What are the two views on reactive systems?

A
  1. A process performs an action and becomes another process (Labelled Transition Systems)
  2. A process changes state and becomes another process (Kripke Structure)
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

What is a Kripke Structure? Formal definition

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

What is a Kripke Structure? Informal definition

A

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.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

What is a path “pi” in a Kripke structure?

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

What is PROMELA?

A

A programming language that can be used to model Kripke structures

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

Main Components of a PROMELA Model

A
  1. Type declarations
  2. Channel declarations
  3. Variable declarations
  4. Process declarations
  5. “init” process
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

Data Types in PROMELA

A
  1. Five Basic types:
    - bit (0/1)
    - bool (false/true)
    - byte (0, 255)
    - short(many more integers)
    - int (even more integers)
  2. Arrays:
    - e.g., byte a[27] or bit flags[4]
  3. Records:
    - e.g.,:

typedef Rectangle {
int width;
int height;
}
Rectangle rr;
rr.width = …

  1. Message Types/ Enumerations:
    - e.g.,:
    mtype:fruit = {apple, pear};
    mtype:size = {small, medium};
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

Defining a process body in PROMELA

A

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
}

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

Executability of Statements in PROMELA:

A

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)

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

Non-deterministic choice in PROMELA

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

Loops in PROMELA

A

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 well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

How can one instantiate a process in PROMELA?

A

Processes can be instantiated by using the run keyword.

E.g., for process bruh, run(bruh) instantiates this process

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
17
Q

When are run statements blocked?

A

when 255 procesess are already running

18
Q

What does the keyword active mean for processes? What does active[N] proctype bruh mean?

A

Means that the process is instantiated from the start.

Means that N instances of the process are instantiated from the start.

19
Q

How is control flow passed in between processes in PROMELA?

A

all processes are executed concurrently, independently of the speed of the behaviour

20
Q

How do processes communicate in between each other in PROMELA?

A

through global variables and channels

21
Q

Global variables in PROMELA

A

defined at the top-level

can be read and updated just like local variables

22
Q

Atomic Statements in PROMELA

A

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

23
Q

Types of Properties Able to be Checked By Spin

A
  1. Deadlocks
  2. Unreachable code
  3. Assertions
  4. Linear Time Logic (LTL) Formulas
24
Q

What are deadlocks in PROMELA?

A

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

25
Q

What are unreachable states in promela?

A

a segment of a program that can never be executed during the normal flow of the program due to conditional statements or other logical constraints

26
Q

What are assertions in promela?

A

statements embedded in code to express expected conditions that should always hold true, and they are used for runtime verification to detect and handle unexpected situations

27
Q

What are LTL formulas in promela?

A

formalism for specifying properties of system behaviours over time, allowing the expression of temporal logic properties such as “eventually”, “always”, and “until” to verify system correctness

28
Q

What are safety properties in PROMELA?

A

properties checking that nothing bad ever happens

e.g., the car never crashes or the system is deadlock free

29
Q

Checking Safety Properties in PROMELA

A

involves finding a path leading to the “bad” thing

if such a path does not exist, the property is satisfied

safety properties can be expressed by placing assertions in the model

30
Q

What are liveness properties in PROMELA?

A

properties specifying that something good will eventually happen

e.g., the system eventually terminates, or if X occurs, then Y eventually occurs

31
Q

Checking Liveness Properties in SPIN

A

involves finding a loop in which the good thing never happens

if such a loop does not exist, then the property is satisfied

liveness properties can be expressed as LTL formulas, which can be added to a model

32
Q

How does deadlock checking work in PROMELA?

A

SPIN reports deadlocks as invalid end states

only valid end states are at proctype’s }

other valid end states can be indicated using the keyword end

33
Q

How to perform a random simulation of the model?

A

spin -p -g -l lock.pml

34
Q

How to perform an interactive simulation of the model?

A

spin -i -p -g -l lock.pml

35
Q

How to generate a verifier for the model and execute it?

A
  1. Generate verifier:

spin -a lock.pml

  1. Build the verifier:

gcc -DNOREDUCE -o pan pan.c

  1. Execute:

./pan

Or all in one check:

spin -run -noreduce lock.pml

36
Q

How to run a counterexample in SPIN?

A

spin -t -p -g -l lock.pml

37
Q

Channels in PROMELA

A

chan = [] of {, ,…, }

e.g., chan c = [0] of {bit, Record}
e.g., chan c[N] = [2] of {mtype, bit}

38
Q

Synchronous Channels

A

have dimension 0

requires sender and receiver processes to be synchronised in time, blocking each other until communication occurs

39
Q

Asynchronous Communication

A

have dimension > 0

allows processes to send and receive messages independently, decoupling sender and receiver actions without immediate synchronisation

40
Q

Sending and Receiving messages

A

ch ! 1; // sends byte 1 across channel ch
ch ? 1; // receives byte 1 across channel ch

41
Q

Message passing vs Message Testing

A

Message Passing
- ch ? , , …, , where var1, var2,…, varn represent variables that will be assigned values from the received message

Message Testing:
- ch ? , , …, , where const1, const2,…, constn represent constants that you check whether exist within the message sent

eval(var1) is the equivalent of const1 but for the value inside var1