uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Design and Verification of Component Based Real-Time Systems
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2009 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

The design of embedded real-time systems is becoming more and more challengingdue to the increasing complexity of new hardware platforms, requirements onnew system functionality, and economical constraints on system development.Component based design has been successful for the development of general-purposecomputer systems such as destop and e-business.In this thesis, a component based design technology is presentedfor embedded real-time systems, that includes a component model SaveCCMand a software tool Uppaal PORT for the formal verification of SaveCCMcomponents and systems.The main contributions of the thesis include a timed semantics ofSaveCCM and a model-checking technique for component-based timed systemsbased on partial order reduction.

To develop a formal semantics for SaveCCM, a core language is presentedto describe SaveCCM components in terms of timed automata.The language is particularly designed for analysis, as it has a small numberof primitive constructs that can easily be translated to the formalismexpected by an analysis technique of interest.The core constructs also preserve the structure of the original system,which can be exploited for model-checking.To develop a scalable verification technique for SaveCCM,partial order reduction is studied as a technique to improve efficiencyfor model-checking, based on independence between parallel activities.For component based systems modelled as timed automata, time may not pass inone component unless the same amount of time passes in all other components.This global nature of time implies a dependency between delay transitions,which is a major obstacle to partial order reduction for timed systems.A known technique to resolve this dependency is to introduce local timescales, which are then synchronized when components communicate.In this thesis, it is demonstrated that the local time approach works wellfor SaveCCM when the system structure is exploited, since communication isrestricted by the structure, which also restricts the need for synchronization.The partial order reduction technique is implemented in the Uppaal PORT tool.This tool and the component model SaveCCM have been validated in twocase studies: an adaptive cruise controller and a turntable production system.

Finally, to assist modelling of SaveCCM systems, two modelling extensionsare introduced. First, component execution is described in terms oftask automata, which can be used for schedulability analysis.The second extension introduces priorities for timed automata, as the conceptof priorities is much used in real-time systems.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2009. , 171 p.
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 87
Keyword [en]
Component Based Software, Real-Time Systems, Model Checking, Verification, Timed Automata, Embedded Systems
National Category
Computer Science
Research subject
Computer Science
URN: urn:nbn:se:uu:diva-101423ISBN: 978-91-554-7537-6OAI: oai:DiVA.org:uu-101423DiVA: diva2:213061
Public defence
2009-06-12, Room 2446, Polacksbacken, Lägerhyddsvägen 2D, Uppsala, 13:15 (English)
Available from: 2009-05-20 Created: 2009-04-27 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text
Buy this publication >>

By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 682 hits
ReferencesLink to record
Permanent link

Direct link