Modelling and analysis of real-time coordination patterns

Leiden Repository

Modelling and analysis of real-time coordination patterns

Title: Modelling and analysis of real-time coordination patterns
Author: Kemper, Stephanie
Publisher: BOXPress BV
Issue Date: 2011-12-20
Keywords: Real-time systems
Coordination patterns
SAT and SMT-solving
Abstraction refinement
Tool implementation
Abstract: 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.
Description: Promotores: F.S. de Boer, F. Arbab
With Summary in Dutch
Faculty: Faculteit der Wiskunde en Natuurwetenschappen
Citation: Kemper, S., 2011, Doctoral Thesis, Leiden University
Series/Report no.: IPA Dissertation Series;2011-24
ISBN: 9789088913600

Files in this item

Description Size View
application/pdf Full Text 2.404Mb View/Open
application/pdf Cover 354.7Kb View/Open
application/pdf Title Pages_Contents 416.0Kb View/Open
application/pdf Chapter 1 199.0Kb View/Open
application/pdf Chapter 2 538.7Kb View/Open
application/pdf Chapter 3 469.1Kb View/Open
application/pdf Chapter 4 486.4Kb View/Open
application/pdf Chapter 5 965.6Kb View/Open
application/pdf Chapter 6 182.6Kb View/Open
application/pdf Appendices 523.6Kb View/Open
application/pdf Abstract 70.20Kb View/Open
application/pdf Summary in Dutch 70.5Kb View/Open
application/pdf Curriculum Vitae_Index_Bibliography 289.7Kb View/Open
application/pdf Propositions 44.63Kb View/Open

This item appears in the following Collection(s)