Trace-based Bounded Verification of Embedded Systems. Huang, Z. & Mitra, S. 2012.
abstract   bibtex   
This paper presents a technique that combine simulations and formal analysis for verifying embedded systems. It presents an algorithm which takes a simulation trace and a system model as input, and computes and overapproximation of the bounded reachable states of any execution that may have produced the trace. This enables approximate verification of bounded safety properties. Implementation of the algorithm in a software tool works with traces and models from Mathworks Simulink/Stateflow. Experimental evaluation of the tool in analyzing several benchmark systems with linear and nonlinear dynamics, and with upto 10 continuous dimensions, hints at the practical applicability of this approach.
@Article{HM:ESL2012,
  Title                    = {Trace-based Bounded Verification of Embedded Systems},
  Author                   = {Zhenqi Huang and Sayan Mitra},
  Year                     = {2012},

  Abstract                 = {This paper presents a technique that combine simulations and formal analysis for verifying embedded systems. It presents an algorithm which takes a simulation trace and a system model as input, and computes and overapproximation of the bounded reachable states of any execution that may have produced the trace. This enables approximate verification of bounded safety properties. Implementation of the algorithm in a software tool works with traces and models from Mathworks Simulink/Stateflow. Experimental evaluation of the tool in analyzing several benchmark systems with linear and nonlinear dynamics, and with upto 10 continuous dimensions, hints at the practical applicability of this approach.},
  Biburl                   = {http://users.crhc.illinois.edu/mitras/research.html},
  Keywords                 = {Verification},
  Notes                    = {Under review},
  Owner                    = {mitras},
  Timestamp                = {2012.04.02}
}

Downloads: 0