Title :
Modular specification of real-time systems
Author_Institution :
Dept. of Comput. Sci., Tech. Univ. Denmark, Lyngby, Denmark
Abstract :
Duration Calculus, a real-time interval logic, has been embedded in the Z specification language to provide a notation for real-time systems that combines the modularisation and abstraction facilities of Z with a logic suitable for reasoning about real-time properties. In this article the notation is presented through a top-level specification of requirements for a simple air traffic monitoring system, and reasoning is illustrated by a refinement towards a design
Keywords :
air traffic computer control; formal specification; real-time systems; specification languages; Duration Calculus; Z specification language; abstraction facilities; air traffic monitoring system; modular specification; real-time interval logic; real-time systems; reasoning; Air traffic control; Aircraft; Airports; Calculus; Control design; Documentation; Formal specifications; Logic; Monitoring; Real time systems;
Conference_Titel :
Real-Time Systems, 1994. Proceedings., Sixth Euromicro Workshop on
Conference_Location :
Vaesteraas
Print_ISBN :
0-8186-6340-5
DOI :
10.1109/EMWRTS.1994.336871
