DocumentCode
3109640
Title
Correctness of vehicle control systems-a case study
Author
Weinberg, H.B. ; Lynch, Nancy
Author_Institution
Lab. for Comput. Sci., MIT, Cambridge, MA, USA
fYear
1996
fDate
4-6 Dec 1996
Firstpage
62
Lastpage
72
Abstract
Several example vehicle deceleration manoeuvres arising in automated transportation systems are specified, and their correctness verified, using the hybrid I/O automaton model of (Lynch et al., 1995). All system components are formalized using hybrid I/O automata, and their combination described using automaton composition. The proofs use invariant assertions, simulation mappings, and differential calculus
Keywords
acceleration control; automata theory; differentiation; formal verification; real-time systems; transport control; vehicles; automated transportation systems; case study; correctness verification; differential calculus; hybrid I/O automata; hybrid input output automata; invariant assertions; real time systems; simulation mappings; vehicle control systems correctness; vehicle deceleration manoeuvres; Automata; Automatic control; Calculus; Computer aided software engineering; Computer science; Control systems; Laboratories; Timing; Transportation; Vehicles;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Systems Symposium, 1996., 17th IEEE
Conference_Location
Los Alamitos, CA
ISSN
1052-8725
Print_ISBN
0-8186-7689-2
Type
conf
DOI
10.1109/REAL.1996.563701
Filename
563701
Link To Document