Verification via Digitized Models of Real-Time Hybrid Systems

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Dang Van Hung Articles by Ko Kwang Il

Third Asia-Pacific Software Engineering Conference (APSEC'96)

Seoul, SOUTH KOREA

December 04-December 07

ISBN: 0-8186-7638-8

	ASCII Text	x
	Dang Van Hung, Ko Kwang Il, "Verification via Digitized Models of Real-Time Hybrid Systems," Asia-Pacific Software Engineering Conference, pp. 4, Third Asia-Pacific Software Engineering Conference (APSEC'96), 1996.

	BibTex	x
	@article{ 10.1109/APSEC.1996.566735, author = {Dang Van Hung and Ko Kwang Il}, title = {Verification via Digitized Models of Real-Time Hybrid Systems}, journal ={Asia-Pacific Software Engineering Conference}, volume = {0}, year = {1996}, isbn = {0-8186-7638-8}, pages = {4}, doi = {http://doi.ieeecomputersociety.org/10.1109/APSEC.1996.566735}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Asia-Pacific Software Engineering Conference TI - Verification via Digitized Models of Real-Time Hybrid Systems SN - 0-8186-7638-8 SP EP A1 - Dang Van Hung, A1 - Ko Kwang Il, PY - 1996 KW - formal specification; specification; verification; real-time hybrid systems; digitized models; duration calculus; int formula; system clock; digital states; analog states; time reasoning; distributed systems; intuitive model; communication protocols; natural induction rules VL - 0 JA - Asia-Pacific Software Engineering Conference ER -

Dang Van Hung, Int. Inst. for Software Technol., United Nations Univ., Macau

Ko Kwang Il, Int. Inst. for Software Technol., United Nations Univ., Macau

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.1996.566735

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.

Index Terms:

formal specification; specification; verification; real-time hybrid systems; digitized models; duration calculus; int formula; system clock; digital states; analog states; time reasoning; distributed systems; intuitive model; communication protocols; natural induction rules

Citation:

Dang Van Hung, Ko Kwang Il, "Verification via Digitized Models of Real-Time Hybrid Systems," apsec, pp.4, Third Asia-Pacific Software Engineering Conference (APSEC'96), 1996

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.