Title :
Discrete-time hybrid modeling and verification
Author :
Torrisi, Fabio Danilo ; Bemporad, Alberto
Author_Institution :
Autom. Control Lab., Eidgenossische Tech. Hochschule, Zurich, Switzerland
Abstract :
For hybrid systems described by interconnections of linear dynamical systems and logic devices, we recently (A. Bemporad et al., 2000, 2001) proposed mixed logical-dynamical (MLD) systems and the language HYSDEL (HYbrid System DEscription Language) as a modeling tool. For MLD models, we developed a reachability analysis algorithm which combines forward reach-set computation and feasibility analysis of trajectories by linear and mixed-integer linear programming. In this paper, the versatility of the overall analysis tool is illustrated in the verification of an automotive cruise control system for a car with a robotized manual gear shift
Keywords :
automobiles; control system analysis; discrete time systems; formal verification; integer programming; interconnected systems; linear programming; linear systems; logic devices; modelling; reachability analysis; robots; simulation languages; HYSDEL; Hybrid System Description Language; automotive cruise control system verification; car; discrete-time hybrid modeling; discrete-time hybrid systems verification; forward reach-set computation feasibility analysis; interconnected systems; linear dynamical systems; logic devices; mixed logical-dynamical systems; mixed-integer linear programming; reachability analysis algorithm; robotized manual gear shift; trajectories; Algorithm design and analysis; Automata; Automatic control; Automotive engineering; Control system synthesis; Control systems; Formal verification; LAN interconnection; Reachability analysis; Safety;
Conference_Titel :
Decision and Control, 2001. Proceedings of the 40th IEEE Conference on
Conference_Location :
Orlando, FL
Print_ISBN :
0-7803-7061-9
DOI :
10.1109/.2001.980716
