Real-Time Symbolic Model Checking for Hard Real-Time 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 Y. Tachi Articles by S. Yamane

Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99)

Hong Kong, China

December 13-December 15

ISBN: 0-7695-0306-3

	ASCII Text	x
	Y. Tachi, S. Yamane, "Real-Time Symbolic Model Checking for Hard Real-Time Systems," Real-Time Computing Systems and Applications, International Workshop on, pp. 496, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999.

	BibTex	x
	@article{ 10.1109/RTCSA.1999.811305, author = {Y. Tachi and S. Yamane}, title = {Real-Time Symbolic Model Checking for Hard Real-Time Systems}, journal ={Real-Time Computing Systems and Applications, International Workshop on}, volume = {0}, year = {1999}, issn = {1530-1427}, pages = {496}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.1999.811305}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Real-Time Computing Systems and Applications, International Workshop on TI - Real-Time Symbolic Model Checking for Hard Real-Time Systems SN - 1530-1427 SP EP A1 - Y. Tachi, A1 - S. Yamane, PY - 1999 KW - real-time systems KW - real-time symbolic model checking KW - real-time temporal logic KW - timed automaton VL - 0 JA - Real-Time Computing Systems and Applications, International Workshop on ER -

Y. Tachi, JAIST

S. Yamane, Kagoshima University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTCSA.1999.811305

We develop real-time symbolic model checking. Real-time systems can be described using timed automata. Although there exist model-checking algorithms for timed automata, the problem is intractable. In this paper, we propose a symbolic model-checking method as follows: Real-time systems can be expressed by BDDs. Symbolic computations are realized by approximations. The fixpoint computations of real-time temporal logic TCTL are realized by both forward and backward computations.

Index Terms:

real-time systems, real-time symbolic model checking, real-time temporal logic, timed automaton

Citation:

Y. Tachi, S. Yamane, "Real-Time Symbolic Model Checking for Hard Real-Time Systems," rtcsa, pp.496, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999

Peer Review Notice | Give Us Feedback

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