ARTES Lic Thesis
A Formal Approach to the Analysis of
Software Architechtures for Real Time Systems
Respondent: Anders Wall, Mälardalen University and Uppsala University
Opponent: Martin Törngren, Royal Institute of Technology, Stockholm
Link to complete thesis
TIME & PLACE: Sept 15, 2000 at13.15, room V226 Dept of Computer Engineering, MDH, Västerås
ABSTRACT
A software architecture is a highlevel design description of a software
system. In terms of the architecture, early design decisions can be
analyzed to improve the quality of a real time software system, which
depends very much on how it is structured rather than how it is
implemented. Architectural analysis techniques vary in their degree of
formality. The least formal is based on reviews and scenarios, whereas
the most formal analysis methods are based on mathematics. In this
thesis, we propose to use a formal approach to software architectural
analysis. We use networks of timed automata to model the architecture of
real time systems and transform architectural analysis problems to
reachability problems that can be checked by the existing tools e.g. UPPAAL
for timed automata. The typical properties that can be handled using this
approach are schedulability and safety properties.
As the first technical contribution, we extend the classic model of
timed automata with a notion of real time tasks. This yields a general
model for realtime systems in which tasks may be periodic and
nonperiodic. We show that the schedulability problem for the extended
model can be transformed to a reachability problem for standard timed
automata, and thus it can be checked by existing modelchecking tools,
e.g. Uppaal for timed automata. As the second contribution, we present a
method to check general high level temporal requirements e.g. timing
constraints on data flowing in multirate transactions, which can not be
handled by traditional approach to schedulability analysis. We have
developed an algorithm that given a data dependency model and a schedule
for a transaction constructs a timed automaton describing the behavior
of the transaction. Thus, by using existing verification tools we can
verify that a given architecture is schedulable and more importantly, it
is correctly constructed with respect to the high level temporal
constraints.
