Chapter 1 - Modeling Flashcards
Lecture 1
Transformational systems
- 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
Interactive systems
- 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
Reactive systems
- 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
Discrete behavior
- behavior interpreted as sequence of events and states
- states remain unchanged between events
Continuous behavior
- the state of the system changes continuously over time
Hybrid behavior
- continuous and discrete aspects are relevant
- in Cyber-Physical Systems
Timed behavior
- 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
Stochastic behavior
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
Data-intensiveness
- 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.
Labeled Transition Systems (LTSs)
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)
LTS (formal def.)
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.
Path in LTS
is a sequence of transitions (si, ai, s’i) that follow each other.
Word accepted by an LTS
— 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.
Language accepted by TS
-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
When modeling real-life systems, it is often convenient to…
- consider variables
- consider guarded transitions
- side-effects of transitions on variables
How do the processes communicate?
by sending messages over channels.
Asynchronous messages:
messages can be stored in a FIFO buffer.
Synchronous messages:
sending and receiving together are single event. (Special case of asynchronous msgs with buffer of size 0)
what does “c!press” mean?
‘press’ is sent over channel c
what does “c?press” mean?
‘press’ is received over channel c
summary LTSs
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.
