Complex systems are by necessity hierarchically organized. Decomposition into subsystems allows for intellectual control, as well as enabling different subsystems to be created by distinct teams. This decomposition affects both requirements and architecture. The architecture describes the structure and this affects how requirements '"flow down" to each subsystem. Moreover, discoveries in the design process may affect the requirements. Demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem. In this paper, we present a medical device case example where we apply an iterative approach to architecture and verification based on software architectural models. We represent the hierarchical composition of the system in the Architecture Analysis and Design Language (AADL), and use an extension to the AADL language to describe the requirements at different levels of abstraction for compositional verification. The component-level behavior for the model is described in Simulink/Stateflow. We assemble proofs of system level properties by using the Simulink Design Verifier to establish component-level properties and an open-source plug-in for the OSATE AADL environment to perform the compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design and verification of detailed behavioral models, and to scale formal analysis to large software systems.
|Original language||English (US)|
|Title of host publication||HILT 2013 - Proceedings of the ACM Conference on High Integrity Language Technology|
|Number of pages||14|
|State||Published - 2013|
|Event||2013 ACM SIGAda Annual International Conference on High Integrity Language Technology, HILT 2013 - Pittsburgh, PA, United States|
Duration: Nov 10 2013 → Nov 14 2013
|Name||HILT 2013 - Proceedings of the ACM Conference on High Integrity Language Technology|
|Other||2013 ACM SIGAda Annual International Conference on High Integrity Language Technology, HILT 2013|
|Period||11/10/13 → 11/14/13|
Copyright 2013 Elsevier B.V., All rights reserved.
- compositional verification
- cyber physical systems
- system decomposition