Compositional verification of a medical device system

Research output: Chapter in Book/Report/Conference proceedingConference contribution

34 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationHILT 2013 - Proceedings of the ACM Conference on High Integrity Language Technology
Pages51-64
Number of pages14
DOIs
StatePublished - 2013
Event2013 ACM SIGAda Annual International Conference on High Integrity Language Technology, HILT 2013 - Pittsburgh, PA, United States
Duration: Nov 10 2013Nov 14 2013

Publication series

NameHILT 2013 - Proceedings of the ACM Conference on High Integrity Language Technology

Other

Other2013 ACM SIGAda Annual International Conference on High Integrity Language Technology, HILT 2013
CountryUnited States
CityPittsburgh, PA
Period11/10/1311/14/13

Bibliographical note

Copyright:
Copyright 2013 Elsevier B.V., All rights reserved.

Keywords

  • compositional verification
  • cyber physical systems
  • system decomposition

Fingerprint Dive into the research topics of 'Compositional verification of a medical device system'. Together they form a unique fingerprint.

Cite this