Paper Info
Title
A bounded model checking tool for periodic sample-hold systems
Abstract
Safety verification of a plant together with its controller is an important part of controller design. If the controller is implemented in software, then a formal model such as hybrid automata is needed to model the composite system. However, classic hybrid automata scale poorly for complex software controllers due to their eager representation of discrete states. In this paper we present safety verification for software controllers without constructing hybrid automata. Our approach targets a common class of software controllers, where the plant is periodically sampled and actuated by the controller. The resulting systems exhibit a regular alternation of discrete steps and fixed length continuous-time evolution. We show that these systems can be verified by a combination of SMT solving and Taylor models. SMT formulas accurately capture control software in a compact form, and Taylor models accurately capture continuous trajectories up to guaranteed error bounds.
Year
DOI
Venue
2014
10.1145/2562059.2562134
HSCC
Keywords
Field
DocType
bounded model checking tool,smt formula,classic hybrid automata scale,periodic sample-hold system,discrete step,taylor model,software controller,complex software controller,discrete state,control software,controller design,hybrid automaton
Control theory,Taylor models,Model checking,Control theory,Automaton,Control engineering,Software,Periodic graph (geometry),Mathematics,Bounded function,Alternation (linguistics)
Conference
Citations 
PageRank 
References 
4
0.40
11
Authors
2
Name
Order
Citations
PageRank
Gabor Simko1427.06
Ethan K. Jackson220415.30