TY - GEN
T1 - Complex system design verification using assumption generation
AU - Mehrpouyan, Hoda
AU - Giannakopoulou, Dimitra
AU - Brat, Guillaume
AU - Tumer, Irem Y.
AU - Hoyle, Chris
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - Assumption generation
KW - Complex system verification
KW - Compositional verification
KW - Conceptual design
UR - http://www.scopus.com/inward/record.url?scp=84896971223&partnerID=8YFLogxK
U2 - 10.1115/DETC2013-13206
DO - 10.1115/DETC2013-13206
M3 - Conference contribution
AN - SCOPUS:84896971223
SN - 9780791855867
T3 - Proceedings of the ASME Design Engineering Technical Conference
BT - 33rd Computers and Information in Engineering Conference
T2 - ASME 2013 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, IDETC/CIE 2013
Y2 - 4 August 2013 through 7 August 2013
ER -