Reduced models for efficient CCS verification

被引:23
作者
Barbuti, R
Francesco, N
Santone, A
Vaglini, G
机构
[1] Univ Pisa, Dipartimento Informat, I-56125 Pisa, Italy
[2] Univ Pisa, Dipartimento Ingn Informaz, I-56125 Pisa, Italy
[3] Univ Sannio, Fac Ingn, RCOST, I-82100 Benevento, Italy
关键词
model checking; state explosion problem; CCS;
D O I
10.1007/s10703-005-1634-6
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Verification of a concurrent system can be accomplished by model checking the properties on a structure representing the system; this structure is, in general, a transition system which contains a prohibitive number of states. In this paper, we apply a method to reduce the state explosion problem by pointing out the events of the system to be ignored on the basis of the property to be verified. We evaluate the method by means of a real application used as a case study: the system is specified by a CCS program, then the program is reduced by means of syntactic rules; afterwards, the corresponding transition system is built by means of a non-standard operational semantics, which performs further reductions during the construction. Prototype tools perform both kinds of reductions; finally the required properties are checked by means of the model checkers of the CWB-NC.
引用
收藏
页码:319 / 350
页数:32
相关论文
共 37 条
[1]  
AZIZ A, 1994, LECT NOTES COMPUTER, V818, P324
[2]  
Barbuti R, 1999, SOFTWARE PRACT EXPER, V29, P1123, DOI 10.1002/(SICI)1097-024X(199910)29:12<1123::AID-SPE275>3.0.CO
[3]  
2-6
[4]   Selective Mu-calculus and formula-based equivalence of transition systems [J].
Barbuti, R ;
De Francesco, N ;
Santone, A ;
Vaglini, G .
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1999, 59 (03) :537-556
[5]  
BARBUTI R, 1997, P FORTE 10 PSTV 17 9, P519
[6]  
BENSALEM S, 1992, LECT NOTES COMPUTER, V663, P260
[7]   INTRODUCTION TO THE ISO SPECIFICATION LANGUAGE LOTOS [J].
BOLOGNESI, T ;
BRINKSMA, E .
COMPUTER NETWORKS AND ISDN SYSTEMS, 1987, 14 (01) :25-59
[8]  
BOUAJJANI A, 1991, LECT NOTES COMPUT SC, V510, P76
[9]   MINIMAL STATE GRAPH GENERATION [J].
BOUAJJANI, A ;
FERNANDEZ, JC ;
HALBWACHS, N ;
RAYMOND, P ;
RATEL, C .
SCIENCE OF COMPUTER PROGRAMMING, 1992, 18 (03) :247-269
[10]  
BRADFIELD J, 1990, LECT NOTES COMPUT SC, V458, P115