loading...
Scalable compositional verification of high-level real-time concurrent systems from 107 to 1085 states
Seoul, Korea October 30-November 01
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTCSA.1996.554967Third International Workshop on Real- ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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 -
 
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
Usage of this product signifies your acceptance of the Terms of Use.