Title :
Verification via digitized models of real-time hybrid systems
Author :
Van Hung, Dang ; Kwang, Ko, II
Author_Institution :
Int. Inst. for Software Technol., United Nations Univ., Macau
Abstract :
The paper presents an approach to the specification and verification of real-time hybrid systems using duration calculus (DC). By introducing a formula int to DC to express the intervals of time between two ticks of the system clock, it is shown that DC can be used to specify both the digital states and the analog states as well as to reason about time in distributed systems. The authors illustrate their approach by giving an intuitive model for the communication protocols in which the verification can be done by using the familiar natural induction rules
Keywords :
distributed processing; formal specification; formal verification; process algebra; protocols; real-time systems; temporal logic; temporal reasoning; timing; analog states; communication protocols; digital states; digitized models; distributed systems; duration calculus; int formula; intuitive model; natural induction rules; real-time hybrid systems; specification; system clock; time reasoning; verification; Analog computers; Boolean functions; Calculus; Clocks; Information technology; Logic; Paper technology; Protocols; Real time systems; Timing;
Conference_Titel :
Software Engineering Conference, 1996. Proceedings., 1996 Asia-Pacific
Conference_Location :
Seoul
Print_ISBN :
0-8186-7638-8
DOI :
10.1109/APSEC.1996.566735
