Modelling and Analysis of Real-Time Coordination Patterns

Present-day embedded software systems need to support an increasing number of features and formalisms; the two most important ones being handling of real-time, and the possibility to develop the system in a modular, component-based way. To ensure that the behaviour of the final system is correct and safe, it needs to be verified before it is being put into operation. This requires formal models to model the system, and formal methods to analyse the formal model and verify certain properties of it. In this thesis, we propose both formal models and formal methods for component-based real-time systems and their coordination patterns. We present a translation from a number of formal models into a representation in propositional logic with linear arithmetic, which allows to use well-established SAT and SMT solver tools to analyse the underlying system. We present an abstraction technique on the representation, that increases the manageable system size by removing parts that are considered irrelevant to the verification of a particular property. We prove the applicability and usability of our framework with a tool implementation, that supports the design and analysis process of component-based real-time systems.

• View at Worldcat

Free Full Text ( Author Manuscript , 1mb )