Verifying switched-mode computer controlled systems
Tóm tắt
This paper presents a new approach to verifying properties of computer control systems with periodic sampling when the control programs include both continuous-variable computations and discrete-state transitions (mode switching). We focus on the novel aspects of the approach, which are (1) a formal model for hybrid systems with continuous-time and discrete-time behavior and (2) a method for computing conservative approximations to the sets of reachable states. The formal model and computational routines are incorporated into CheckMate, a MATLAB-based tool for verification of properties of hybrid dynamic systems. This tool is being applied to the verification of embedded controllers in automotive engines.
Từ khóa
#Control systems #Sampling methods #Vehicle dynamics #Mathematical model #Automatic control #Computational modeling #Automotive engineering #Automata #Computer languages #EnginesTài liệu tham khảo
10.1109/9.948467
10.1145/177492.177725
chutinan, 1999, Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations, Hybrid Systems Computation Control 2nd Int Workshop HSCC 99, 10.1007/3-540-48983-5_10
10.1109/ACC.1995.532313
butts, 0, Ford Motor Company private correspondence
10.1109/CACSD.2002.1036936
10.1109/CDC.2001.980711
10.1109/CACSD.2000.900208
10.1016/S0005-1098(98)00179-4
10.1109/CDC.2001.980198
clarke, 1999, Model checking
10.1109/LICS.1996.561342
10.1109/32.489079
van der schaft, 2000, An Introduction to Hybrid Dynamical Systems, 10.1007/BFb0109998
10.1109/ACC.2000.879487