Submitted: September 2009
Abstract
This bachelor thesis presents a tool for choosing a sensible ordering of smaller models while incrementally building system models by compositional aggregation. It is important that this “sensible ordering”, or “smart ordering”, is determined automatically by this tool, as opposed to the currently used way of determining an order by semiautomatic heuristics. The goal is to close the existing gap at that point in automated model checking.
First, the reader is introduced to the problem, a loose definition of smart ordering is given, and thereby also the need for such an ordering is motivated.
After that the underlying concept how to find a smart ordering is explained in greater detail, the reader will learn about metrics and which metrics are used to facilitate the finding of a smart ordering.
A tool is presented that implements the finding of a smart ordering by using metrics.
To back up the notion of smart ordering, a few case studies are shown and analyzed by comparing figures of “man-made” ordering and smart ordering.
Lastly, there is a summarization of all findings, as well as an outlook on further possible work.