Model-based Specification Reconstruction
pdf
This poster surveys results in the area of specification reconstruction for system models obtained by teams from the University of Maryland and Fraunhofer Center as part of the NSF CPS Frontier program "CyberCardia". The specification-reconstruction problem is this: given a system model, and a template of a property describing a pattern of behavior, determine how to complete the template so that the resulting property holds for all behaviors of the system. In one approach studied by the team, the templates take the form of linear temporal logic (LTL) formulas with "holes", or missing sub-formulas, while the models are so-called Kripke structures, or finite-state machines describing how the system executes. The team pioneered new strategies for "query checking", or solving for the holes in the LTL formulas, that use a correspondence between LTL and finite-state machines called Buechi automata. In the second approach studied by the team, the templates are system invariants, or relationships intended always to hold between different state variables in the model, while the system models are given in the MATLAB® / Simulink® / Stateflow® notations of the The MathWorks, Inc. In this case, data-mining techniques are used to extract prospective invariants from simulation runs of the model, with additional automated testing then used to identify false invariants. The latter approach is studied experimentally on a variety of Simulink models taken from the automotive and medical-device domains.
Submitted by Rance Cleaveland
on
This poster surveys results in the area of specification reconstruction for system models obtained by teams from the University of Maryland and Fraunhofer Center as part of the NSF CPS Frontier program "CyberCardia". The specification-reconstruction problem is this: given a system model, and a template of a property describing a pattern of behavior, determine how to complete the template so that the resulting property holds for all behaviors of the system. In one approach studied by the team, the templates take the form of linear temporal logic (LTL) formulas with "holes", or missing sub-formulas, while the models are so-called Kripke structures, or finite-state machines describing how the system executes. The team pioneered new strategies for "query checking", or solving for the holes in the LTL formulas, that use a correspondence between LTL and finite-state machines called Buechi automata. In the second approach studied by the team, the templates are system invariants, or relationships intended always to hold between different state variables in the model, while the system models are given in the MATLAB® / Simulink® / Stateflow® notations of the The MathWorks, Inc. In this case, data-mining techniques are used to extract prospective invariants from simulation runs of the model, with additional automated testing then used to identify false invariants. The latter approach is studied experimentally on a variety of Simulink models taken from the automotive and medical-device domains.