Parallel Composition of State Machines with Local Variables
Sagici, Yeliz (2015)
2015
Tietotekniikan koulutusohjelma
Tieto- ja sähkötekniikan tiedekunta - Faculty of Computing and Electrical Engineering
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
Hyväksymispäivämäärä
2015-09-09
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:tty-201508281568
https://urn.fi/URN:NBN:fi:tty-201508281568
Tiivistelmä
Concurrent systems in which components interact are usually complex and have plenty of behaviour. This makes it challenging to design and develop reliable, error-free concurrent systems. One method which has had great successes in finding difficult errors in these kinds of systems involves constructing a state space model of the system and using computer tools for analysing it.
A compact way to present components and systems is by describing them as state machines with local variables. The three process-algebraic operators with which all communication between state machines can be expressed are: parallel composition, hiding, and relational renaming. These three operators can also be replaced with a flexible synchronization rule operator, which uses modeller-defined synchronization rules.
This thesis describes how interacting components modelled as state machines with local variables can be composed in parallel using synchronization rules. Parallel composition is described especially from the point of view of synchronous interaction and data transfer. The thesis also gives an overall picture of a tool which was implemented for this thesis. This tool reads in a set of state machines and synchronization rules, performs the parallel composition, and outputs the resulting system, which is also a state machine with local variables.
A compact way to present components and systems is by describing them as state machines with local variables. The three process-algebraic operators with which all communication between state machines can be expressed are: parallel composition, hiding, and relational renaming. These three operators can also be replaced with a flexible synchronization rule operator, which uses modeller-defined synchronization rules.
This thesis describes how interacting components modelled as state machines with local variables can be composed in parallel using synchronization rules. Parallel composition is described especially from the point of view of synchronous interaction and data transfer. The thesis also gives an overall picture of a tool which was implemented for this thesis. This tool reads in a set of state machines and synchronization rules, performs the parallel composition, and outputs the resulting system, which is also a state machine with local variables.