Chapter 1 - Modeling

Question 1

Transformational systems

Answer 1

• transform input values to output values
• inputs are given at the start of the computation
• output are returned when computation terminates

Examples: computing greatest common divisor, solving traveling salesman problem

Question 2

Interactive systems

Answer 2

• the system interacts with its environment (may include human users)
• the system asks for new input during computation
• usually, computation terminates at some point - but may also conceptually, run forever

Examples: online shops, flight booking application

Question 3

Reactive systems

Answer 3

• the system interacts with its environment (may include human users)
• the system must react to input, external events (instead of asking for it)
• often, the computation has no definitive end - system may, conceptually, run forever

Examples: control SW for planes, cars, robots, satellites, trains, power plants, ATMs, telecommunication systems

Question 4

Discrete behavior

Answer 4

• behavior interpreted as sequence of events and states

- states remain unchanged between events

Question 5

Continuous behavior

Answer 5

• the state of the system changes continuously over time

Question 6

Hybrid behavior

Answer 6

• continuous and discrete aspects are relevant

- in Cyber-Physical Systems

Question 7

Timed behavior

Answer 7

• events must / must not occur within certain time bounds
• time scales can be different, example: flight booking > check in 24h before start
  airbag > open within milliseconds

Question 8

Stochastic behavior

Answer 8

in some systems where some events are known to occur with certain probabilities.

Examples: probabilities of hw faults,
data package lost, behavior of users, probability of virus infection

Question 9

Data-intensiveness

Answer 9

• some system are modeled with simple events > Coffee machine
• more complex concepts must be modeled with more complex data structures > flight data in flight booking application

DIESE EVENTS SIND data intensive.

Question 10

Labeled Transition Systems (LTSs)

Answer 10

is a basic modeling language for modeling reactive systems and are simple variant of automata.

• consisting of states and transitions
• transitions are labeled by actions
• suited for modeling the discrete behavior of concurrent systems (systems with several modules/processes that are executed concurrently and communicate with each other)

Question 11

LTS (formal def.)

Answer 11

TS = (S, Σ, T, I)

• S is a set of states
• I ⊆ S is the set of initial states
• Sigma is an alphabet. > An element in Sigma is called a symbol (or input, event, action)
• T ⊆ S x Σ x S is a transition relation
• A TS is called finite if S and Σ are finite.

Question 12

Path in LTS

Answer 12

is a sequence of transitions (si, ai, s’i) that follow each other.

Question 13

Word accepted by an LTS

Answer 13

— w = e0, e1, e2,… will be accepted if there exists a sequence of states in S, where the first state in sequence is an initial State and (si, ei, si+1) ∈ T from all i ≥ 0.

Question 14

Language accepted by TS

Answer 14

-the set of maximal words accepted by an LTS, written L(TS).

> words have infinite length if there are no deadlocks
words can be finite if there are deadlocks

Question 15

When modeling real-life systems, it is often convenient to…

Answer 15

• consider variables
• consider guarded transitions
• side-effects of transitions on variables

Question 16

How do the processes communicate?

Answer 16

by sending messages over channels.

Question 17

Asynchronous messages:

Answer 17

messages can be stored in a FIFO buffer.

Question 18

Synchronous messages:

Answer 18

sending and receiving together are single event. (Special case of asynchronous msgs with buffer of size 0)

Question 19

what does “c!press” mean?

Answer 19

‘press’ is sent over channel c

Question 20

what does “c?press” mean?

Answer 20

‘press’ is received over channel c

Question 21

summary LTSs

Answer 21

LTSs are simple modeling language for modeling concurrent reactive systems.

• concurrent processes can communicate via handshaking or shared variables
• a network of concurrent LTSs can be composed (|| operator): mapped to another LTS that models the equivalent behavior

LTSs are simple, but

• variables/conditions/assignments extension for richer modeling
• programs written in other languages cam be mapped to LTSs

Certain properties of LTS models can be proven automatically via model-checking.