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

fYear

1996

Firstpage

4

Lastpage

15

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference, 1996. Proceedings., 1996 Asia-Pacific

Conference_Location

Seoul

Print_ISBN

0-8186-7638-8

Type

conf

DOI

10.1109/APSEC.1996.566735

Filename

566735