An Efficiently Checkable Subset of TCTL for Formal Verification of Transition Systems with Delays

Goa, India January 10-January 13

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/ICVD.1999.745163

12th International Conference on VLSI ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	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 Jatindra Kumar Deka Articles by Pallab Dasgupta Articles by P.P. Chakrabarti

	ASCII Text	x
	Jatindra Kumar Deka, Pallab Dasgupta, P.P. Chakrabarti, "An Efficiently Checkable Subset of TCTL for Formal Verification of Transition Systems with Delays," VLSI Design, International Conference on, pp. 294, 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', 1999.

	BibTex	x
	@article{ 10.1109/ICVD.1999.745163, author = {Jatindra Kumar Deka and Pallab Dasgupta and P.P. Chakrabarti}, title = {An Efficiently Checkable Subset of TCTL for Formal Verification of Transition Systems with Delays}, journal ={VLSI Design, International Conference on}, volume = {0}, year = {1999}, issn = {1063-9667}, pages = {294}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICVD.1999.745163}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - VLSI Design, International Conference on TI - An Efficiently Checkable Subset of TCTL for Formal Verification of Transition Systems with Delays SN - 1063-9667 SP EP A1 - Jatindra Kumar Deka, A1 - Pallab Dasgupta, A1 - P.P. Chakrabarti, PY - 1999 VL - 0 JA - VLSI Design, International Conference on ER -

Jatindra Kumar Deka

Pallab Dasgupta

P.P. Chakrabarti

Model checking transition systems with delays using timed logics such as TCTL is an attractive technique for property verification of hardware descriptions. TCTL model checking requires the construction of time regions which depends not only on the timed graph, but also the TCTL formula. This limits the efficiency of a pure top-down approach for model checking. We propose a restricted version of TCTL, namely DCTL, which can be checked in a pure top-down manner without augmenting the region graph a priori.

Citation:

Jatindra Kumar Deka, Pallab Dasgupta, P.P. Chakrabarti, "An Efficiently Checkable Subset of TCTL for Formal Verification of Transition Systems with Delays," vlsid, pp.294, 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', 1999

Peer Review Notice | Give Us Feedback

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