Modular verification of reconfigurable components
2005 (English)In: Component-Based Software Development for Embedded Systems: An Overview of Current Research Trends / [ed] Colin Atkinson, Christian Bunse, Hans-Gerhard Gross and Christian Peper, Springer Berlin/Heidelberg, 2005, Vol. 3778, 59-81 p.Chapter in book (Refereed)
This chapter presents a framework for modular verification of reconfigurable real-time components. The framework enables proving that the reconfiguration of components via aspect weaving provides expected functional and temporal behavior in the reconfigured component. Within the framework we formally represent components and aspects as augmentations of timed automata. The verification is based on two algorithms: an algorithm that extracts necessary information into component verification interfaces, and an algorithm that checks, on an aspect, whether the property is preserved upon reconfiguration. Hence, the method ensures that components are verified only once for a particular property, while the property satisfaction under reconfiguration is checked only on aspects. Verification interfaces for a given property can be reused for multiple aspects and reconfigurations.
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2005. Vol. 3778, 59-81 p.
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 3778
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 3778
Engineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-48113DOI: 10.1007/11591962_4ISBN: 978-3-540-30644-3ISBN: e-978-3-540-31614-5ISBN: 3-540-30644-7OAI: oai:DiVA.org:liu-48113DiVA: diva2:269009