Scheduling of guarded command based models
Degerlund, Fredrik (2012-12-10)
Degerlund, Fredrik
Turku Centre for Computer Science (TUCS)
10.12.2012
Julkaisu on tekijänoikeussäännösten alainen. Teosta voi lukea ja tulostaa henkilökohtaista käyttöä varten. Käyttö kaupallisiin tarkoituksiin on kielletty.
Julkaisun pysyvä osoite on
https://urn.fi/URN:ISBN:978-952-12-2811-7
https://urn.fi/URN:ISBN:978-952-12-2811-7
Tiivistelmä
Formal methods provide a means of reasoning about computer programs
in order to prove correctness criteria. One subtype of formal methods is
based on the weakest precondition predicate transformer semantics and uses
guarded commands as the basic modelling construct. Examples of such
formalisms are Action Systems and Event-B. Guarded commands can intuitively
be understood as actions that may be triggered when an associated
guard condition holds. Guarded commands whose guards hold are nondeterministically
chosen for execution, but no further control flow is present
by default. Such a modelling approach is convenient for proving correctness,
and the Refinement Calculus allows for a stepwise development method. It
also has a parallel interpretation facilitating development of concurrent software,
and it is suitable for describing event-driven scenarios. However, for
many application areas, the execution paradigm traditionally used comprises
more explicit control flow, which constitutes an obstacle for using the above
mentioned formal methods. In this thesis, we study how guarded command
based modelling approaches can be conveniently and efficiently scheduled in
different scenarios. We first focus on the modelling of trust for transactions
in a social networking setting. Due to the event-based nature of the scenario,
the use of guarded commands turns out to be relatively straightforward. We
continue by studying modelling of concurrent software, with particular focus
on compute-intensive scenarios. We go from theoretical considerations to the
feasibility of implementation by evaluating the performance and scalability
of executing a case study model in parallel using automatic scheduling performed
by a dedicated scheduler. Finally, we propose a more explicit and
non-centralised approach in which the flow of each task is controlled by a
schedule of its own. The schedules are expressed in a dedicated scheduling
language, and patterns assist the developer in proving correctness of the
scheduled model with respect to the original one.
in order to prove correctness criteria. One subtype of formal methods is
based on the weakest precondition predicate transformer semantics and uses
guarded commands as the basic modelling construct. Examples of such
formalisms are Action Systems and Event-B. Guarded commands can intuitively
be understood as actions that may be triggered when an associated
guard condition holds. Guarded commands whose guards hold are nondeterministically
chosen for execution, but no further control flow is present
by default. Such a modelling approach is convenient for proving correctness,
and the Refinement Calculus allows for a stepwise development method. It
also has a parallel interpretation facilitating development of concurrent software,
and it is suitable for describing event-driven scenarios. However, for
many application areas, the execution paradigm traditionally used comprises
more explicit control flow, which constitutes an obstacle for using the above
mentioned formal methods. In this thesis, we study how guarded command
based modelling approaches can be conveniently and efficiently scheduled in
different scenarios. We first focus on the modelling of trust for transactions
in a social networking setting. Due to the event-based nature of the scenario,
the use of guarded commands turns out to be relatively straightforward. We
continue by studying modelling of concurrent software, with particular focus
on compute-intensive scenarios. We go from theoretical considerations to the
feasibility of implementation by evaluating the performance and scalability
of executing a case study model in parallel using automatic scheduling performed
by a dedicated scheduler. Finally, we propose a more explicit and
non-centralised approach in which the flow of each task is controlled by a
schedule of its own. The schedules are expressed in a dedicated scheduling
language, and patterns assist the developer in proving correctness of the
scheduled model with respect to the original one.