You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.
The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.
For the reports in this repository we specifically note that
- the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
- the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
- technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
- in other cases, please contact the copyright owner for detailed information
By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.
If you are in doubt, feel free to contact webmaster@ide.mdh.se
A Formal Approach to Analysis of Software Architectures for Real-Time Systems
Note:
See thesis with the same title for PDF or PS file.
Publication Type:
Report - MRTC
Publisher:
Dept. of Computer Systems, Uppsala University and Dept. of Computer Engineering, Mälardalen University
ISRN:
MDH-MRTC-31/2000-1-SE
Abstract
A software architecture is a high-level 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 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 real-time systems in which tasks may be periodic and
non-periodic. 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 model-checking 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 multi-rate 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.
Bibtex
@techreport{Wall424,
author = {Anders Wall},
title = {A Formal Approach to Analysis of Software Architectures for Real-Time Systems},
note = {See thesis with the same title for PDF or PS file.},
number = {ISSN 1404-3041 ISRN MDH-MRTC-31/2000-1-SE},
month = {September},
year = {2000},
publisher = {Dept. of Computer Systems, Uppsala University and Dept. of Computer Engineering, M{\"a}lardalen University},
url = {http://www.es.mdu.se/publications/424-}
}