Component-based software development requires formal specifications to ensure correctness in safety-critical applications. This work is innovative in providing formal semantics for real-time component interactions, enabling derivation of system-level properties and supporting rigorous verification of composed systems.
This technical report presents formalization of component models for real-time systems based on ARINC-653 semantics. The work develops timed transition graphs and formal semantic specifications for component interactions in safety-critical real-time systems, enabling rigorous reasoning about system properties.
The formalization captures component port execution semantics, synchronous and asynchronous interactions, and deadline constraints through timed transition traces. The approach enables formal reasoning about component assemblies and supports derivation of system-level fault propagation templates for health management.
@inproceedings{Dubey2012,
author = {Dubey, Abhishek and {Emfinger}, W. and {Gokhale}, A. and {Karsai}, G. and {Otte}, W. R. and {Parsons}, J. and {Szabo}, C. and {Coglio}, A. and {Smith}, E. and {Bose}, P.},
booktitle = {2012 IEEE Aerospace Conference},
title = {A software platform for fractionated spacecraft},
year = {2012},
month = {mar},
pages = {1-20},
abstract = {A fractionated spacecraft is a cluster of independent modules that interact wirelessly to maintain cluster flight and realize the functions usually performed by a monolithic satellite. This spacecraft architecture poses novel software challenges because the hardware platform is inherently distributed, with highly fluctuating connectivity among the modules. It is critical for mission success to support autonomous fault management and to satisfy real-time performance requirements. It is also both critical and challenging to support multiple organizations and users whose diverse software applications have changing demands for computational and communication resources, while operating on different levels and in separate domains of security. The solution proposed in this paper is based on a layered architecture consisting of a novel operating system, a middleware layer, and component-structured applications. The operating system provides primitives for concurrency, synchronization, and secure information flows; it also enforces application separation and resource management policies. The middleware provides higher-level services supporting request/response and publish/subscribe interactions for distributed software. The component model facilitates the creation of software applications from modular and reusable components that are deployed in the distributed system and interact only through well-defined mechanisms. Two cross-cutting aspects - multi-level security and multi-layered fault management - are addressed at all levels of the architecture. The complexity of creating applications and performing system integration is mitigated through the use of a domain-specific model-driven development process that relies on a dedicated modeling language and its accompanying graphical modeling tools, software generators for synthesizing infrastructure code, and the extensive use of model-based analysis for verification and validation.},
category = {conference},
contribution = {lead},
doi = {10.1109/AERO.2012.6187334},
file = {:Dubey2012-A_software_platform_for_fractionated_spacecraft.pdf:PDF},
issn = {1095-323X},
keywords = {component models, formal semantics, ARINC-653, real-time systems, timed transition graphs, safety-critical systems},
tag = {platform},
month_numeric = {3}
}