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
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;
Conference_Titel :
Real-Time Systems Symposium, 1996., 17th IEEE
Conference_Location :
Los Alamitos, CA
Print_ISBN :
0-8186-7689-2
DOI :
10.1109/REAL.1996.563701
