mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Formal Approach to Analysis of Software Architectures for Real-Time Systems
Mälardalen University, Department of Computer Science and Electronics.
2000 (English)Licentiate thesis, monograph (Other scientific)
Abstract [en]

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.

Place, publisher, year, edition, pages
2000.
Identifiers
URN: urn:nbn:se:mdh:diva-1816OAI: oai:DiVA.org:mdh-1816DiVA, id: diva2:114479
Available from: 2008-11-11 Created: 2008-11-11

Open Access in DiVA

No full text in DiVA

Search in DiVA

By author/editor
Wall, Anders
By organisation
Department of Computer Science and Electronics

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 65 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf