Discrete-time hybrid modeling and verification

Author

Torrisi, Fabio Danilo ; Bemporad, Alberto

Author_Institution

Autom. Control Lab., Eidgenossische Tech. Hochschule, Zurich, Switzerland

Volume

3

fYear

2001

fDate

2001

Firstpage

2899

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Decision and Control, 2001. Proceedings of the 40th IEEE Conference on

Conference_Location

Orlando, FL

Print_ISBN

0-7803-7061-9

Type

conf

DOI

10.1109/.2001.980716

Filename

980716