Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2527269.2527272 | HILT |
Keywords | Field | DocType |
large software system,complex system,different subsystems,simulink design verifier,aadl language,verification tool,osate aadl environment,compositional verification,system level property,medical device system,design language,cyber physical systems | Functional verification,Programming language,Computer science,Verification,Real-time computing,Software system,Runtime verification,Architecture Analysis & Design Language,Stateflow,High-level verification,Software verification | Conference |
Volume | Issue | ISSN |
33 | 3 | 1094-3641 |
Citations | PageRank | References |
26 | 1.05 | 22 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Anitha Murugesan | 1 | 44 | 5.21 |
| Michael W. Whalen | 2 | 1096 | 70.54 |
| Sanjai Rayadurgam | 3 | 284 | 29.86 |
| Mats P.E. Heimdahl | 4 | 192 | 9.66 |