Complex system design verification using assumption generation

Hoda Mehrpouyan, Dimitra Giannakopoulou, Guillaume Brat, Irem Y. Tumer, Chris Hoyle

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

Abstract

In the era of large complex systems with continuous and discrete event components, it is critical to establish a complete design verification strategy to determine whether a system satisfies certain safety properties. However, traditional approaches for the verification of such a complex system lack the ability to take into account all possible system states, efficiently model all component interactions, and accurately quantify the risks and uncertainties. This paper presents a methodology for system-level design of complex systems verification based on compositional model checking. This methodology relies on assumption generation and on the domain independent compositional rules for correctness proof of the design of physical systems. The objective is to present a case study for applying the existing automated compositional verification techniques and observing the characteristics of the verification model. The main advantage of this method is that it enables the designer to verify the safety properties of the system without requiring the detail knowledge of the internal actions of the system. The under-approximate context model of the system design is constructed and, in an iterative approach, its safety properties are analyzed until a violation of a property is found and an execution trace called a counter example is produced. In the case of safety requirements violation, the early generation of counter examples leads to faster design verification.

Original languageEnglish
Title of host publication33rd Computers and Information in Engineering Conference
DOIs
StatePublished - 2013
EventASME 2013 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, IDETC/CIE 2013 - Portland, OR, United States
Duration: 4 Aug 20137 Aug 2013

Publication series

NameProceedings of the ASME Design Engineering Technical Conference
Volume2 B

Conference

ConferenceASME 2013 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, IDETC/CIE 2013
Country/TerritoryUnited States
CityPortland, OR
Period4/08/137/08/13

Keywords

  • Assumption generation
  • Complex system verification
  • Compositional verification
  • Conceptual design

Fingerprint

Dive into the research topics of 'Complex system design verification using assumption generation'. Together they form a unique fingerprint.

Cite this