Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states

R
RTCSA
1996
Third International Workshop on Real-Time Computing Systems Application (RTCSA'96)
Abstract - Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states

	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
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Farn Wang

Third International Workshop on Real-Time Computing Systems Application (RTCSA'96)

Seoul, Korea

October 30-November 01

ISBN: 0-8186-7626-4

	ASCII Text	x
	Farn Wang, "Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states," Real-Time Computing Systems and Applications, International Workshop on, pp. 106, Third International Workshop on Real-Time Computing Systems Application (RTCSA'96), 1996.

	BibTex	x
	@article{ 10.1109/RTCSA.1996.554967, author = {Farn Wang}, title = {Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states}, journal ={Real-Time Computing Systems and Applications, International Workshop on}, volume = {0}, year = {1996}, isbn = {0-8186-7626-4}, pages = {106}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.1996.554967}, 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 - Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states SN - 0-8186-7626-4 SP EP A1 - Farn Wang, PY - 1996 KW - formal verification; scalable compositional verification; high-level real-time concurrent systems; compositional CTL mode-checking algorithm; discrete global clock; VERIFAST-2; protocols; truly scalable performance; software recursions VL - 0 JA - Real-Time Computing Systems and Applications, International Workshop on ER -

Farn Wang

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

Inst. of Inf. Sci., Acad. Sinica, Taipei, TaiwanAbstract: A compositional CTL mode-checking algorithm for real-time concurrent systems with a discrete global clock is presented based on a new high-level description model. We implement the algorithm in a system called VERIFAST-2 which has passed the extended General Session Setup Control protocols with concurrency from 5 to 51 threads all in one minute and demonstrated truly scalable performance with respect to the size of concurrency. In this respect, it outperforms HyTech version 1.02 b and VERIFAST-1. Then we discuss how to incorporate R.J. Parikh's classic work on semilinear expressions to verify software recursions.

Index Terms:

formal verification; scalable compositional verification; high-level real-time concurrent systems; compositional CTL mode-checking algorithm; discrete global clock; VERIFAST-2; protocols; truly scalable performance; software recursions

Citation:

Farn Wang, "Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states," rtcsa, pp.106, Third International Workshop on Real-Time Computing Systems Application (RTCSA'96), 1996

Peer Review Notice | Give Us Feedback

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