A Formal Approach to Analysis of Software Architectures for Real-Time Systems

Sammanfattning: A software architecture is a high-level design description of a softwaresystem. In terms of the architecture, early design decisions can beanalyzed to improve the quality of a real time software system, whichdepends very much on how it is structured rather than how it isimplemented. Architectural analysis techniques vary in their degree offormality. The least formal is based on reviews and scenarios, whereasthe most formal analysis methods are based on mathematics. In thisthesis, we propose to use a formal approach to software architecturalanalysis. We use networks of timed automata to model the architecture ofreal time systems and transform architectural analysis problems toreachability problems that can be checked by the existing tools fortimed automata. The typical properties that can be handled using thisapproach are schedulability and safety properties.As the first technical contribution, we extend the classic model oftimed automata with a notion of real time tasks. This yields a generalmodel for real-time systems in which tasks may be periodic andnon-periodic. We show that the schedulability problem for the extendedmodel can be transformed to a reachability problem for standard timedautomata, and thus it can be checked by existing model-checking tools,e.g. UPPAAL for timed automata. As the second contribution, we present amethod to check general high level temporal requirements e.g. timingconstraints on data flowing in multi-rate transactions, which can not behandled by traditional approach to schedulability analysis. We havedeveloped an algorithm that given a data dependency model and a schedulefor a transaction constructs a timed automaton describing the behaviorof the transaction. Thus, by using existing verification tools we canverify that a given architecture is schedulable and more importantly, itis correctly constructed with respect to the high level temporalconstraints.