Nagabhushan Mahadevan, Abhishek Dubey, Gabor Karsai
15th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, ISORC 2012, Shenzhen, China, April 11-13, 2012 2012
Formal specifications are essential for reasoning about correctness in safety-critical systems where informal descriptions lead to ambiguity and errors. This work is significant in providing rigorous mathematical foundations for component interactions that enable automated verification and synthesis of system properties.
This technical report describes formalization of a component model for real-time systems, providing formal semantics for component port execution and interaction patterns. The work develops timed transition traces and formal specifications that enable rigorous analysis of component assemblies in safety-critical applications.
The formalization captures nominal component behavior through timed transition traces, describing port execution semantics for both synchronous and asynchronous interactions. The approach enables derivation of system-level properties and supports formal reasoning about fault propagation and component assembly correctness.
@inproceedings{Mahadevan2012,
author = {Mahadevan, Nagabhushan and Dubey, Abhishek and Karsai, Gabor},
booktitle = {15th {IEEE} International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, {ISORC} 2012, Shenzhen, China, April 11-13, 2012},
title = {Architecting Health Management into Software Component Assemblies: Lessons Learned from the {ARINC-653} Component Mode},
year = {2012},
pages = {79--86},
abstract = {Complex real-time software systems require an active fault management capability. While testing, verification and validation schemes and their constant evolution help improve the dependability of these systems, an active fault management strategy is essential to potentially mitigate the unacceptable behaviors at run-time. In our work we have applied the experience gained from the field of Systems Health Management towards component-based software systems. The software components interact via well-defined concurrency patterns and are executed on a real-time component framework built upon ARINC-653 platform services. In this paper, we present the lessons learned in architecting and applying a two-level health management strategy to assemblies of software components.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/isorc/MahadevanDK12},
category = {selectiveconference},
contribution = {lead},
doi = {10.1109/ISORC.2012.19},
file = {:Mahadevan2012-Architecting_Health_Management_into_Software_Component_Assemblies.pdf:PDF},
keywords = {component models, formal semantics, real-time systems, timed transition traces, safety-critical systems, formal verification},
project = {cps-reliability,cps-middleware},
tag = {platform},
timestamp = {Wed, 16 Oct 2019 14:14:53 +0200},
url = {https://doi.org/10.1109/ISORC.2012.19}
}