Relative liveness: from intuition to automated verification

	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 R. Negulescu Articles by J.A. Brzozowski

Second Working Conference on Asynchronous Design Methodologies

London, England

May 30-May 31

ISBN: 0-8186-7098-3

	ASCII Text	x
	R. Negulescu, J.A. Brzozowski, "Relative liveness: from intuition to automated verification," Asynchronous Circuits and Systems, International Symposium on, pp. 108, Second Working Conference on Asynchronous Design Methodologies, 1995.

	BibTex	x
	@article{ 10.1109/WCADM.1995.514648, author = {R. Negulescu and J.A. Brzozowski}, title = {Relative liveness: from intuition to automated verification}, journal ={Asynchronous Circuits and Systems, International Symposium on}, volume = {0}, year = {1995}, isbn = {0-8186-7098-3}, pages = {108}, doi = {http://doi.ieeecomputersociety.org/10.1109/WCADM.1995.514648}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Asynchronous Circuits and Systems, International Symposium on TI - Relative liveness: from intuition to automated verification SN - 0-8186-7098-3 SP EP A1 - R. Negulescu, A1 - J.A. Brzozowski, PY - 1995 KW - finite automata; multiprocessing programs; multiprocessing systems; program verification; relative liveness; automated verification; finite trace theory; automata; equivalence; safety condition; hierarchical verification theorems; safety; liveness VL - 0 JA - Asynchronous Circuits and Systems, International Symposium on ER -

R. Negulescu, Dept. of Comput. Sci., Waterloo Univ., Ont., Canada

J.A. Brzozowski, Dept. of Comput. Sci., Waterloo Univ., Ont., Canada

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/WCADM.1995.514648

We point out deficiencies of previous treatments of liveness. We define a new liveness condition in two forms: one based on finite trace theory and the other on automata. We prove the equivalence of these two forms. We introduce a safety condition and derive modular and hierarchical verification theorems for both safety and liveness. Finally, we give an algorithm for verifying liveness.

Index Terms:

finite automata; multiprocessing programs; multiprocessing systems; program verification; relative liveness; automated verification; finite trace theory; automata; equivalence; safety condition; hierarchical verification theorems; safety; liveness

Citation:

R. Negulescu, J.A. Brzozowski, "Relative liveness: from intuition to automated verification," async, pp.108, Second Working Conference on Asynchronous Design Methodologies, 1995

Peer Review Notice | Give Us Feedback

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