Reduced Models for Efficient CCS Verification
作者： Roberto Barbuti , Nicoletta De Francesco , Antonella Santone , Gigliola Vaglini
DOI: 10.1007/S10703-005-1634-6
关键词: State (computer science) 、 Basis (linear algebra) 、 Computer engineering 、 Computer science 、 Structure (mathematical logic) 、 Model checking 、 Transition system 、 Operational semantics 、 Algorithm 、 Property (programming)
摘要: Verification of a concurrent system can be accomplished by model checking the properties on structure representing system; this is, in general, transition which contains prohibitive number states. In paper, we apply method to reduce state explosion problem pointing out events ignored basis property verified. We evaluate means real application used as case study: is specified CCS program, then program reduced syntactic rules; afterwards, corresponding built non-standard operational semantics, performs further reductions during construction. Prototype tools perform both kinds reductions; finally required are checked checkers CWB-NC.
springer.com
core.ac.uk
sci-hub.se 参考文章(41)
J. C. Fernandez, A. Kerbrat, L. Mounier, Symbolic Equivalence Checking computer aided verification. pp. 85- 96 ,(1993) , 10.1007/3-540-56922-7_8
Adnan Aziz, Thomas R. Shiple, Vigyan Singhal, Alberto L. Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking computer aided verification. pp. 324- 337 ,(1994) , 10.1007/3-540-58179-0_65
Jan Friso Groote, Jaco van de Pol, A Bounded Retransmission Protocol for Large Data Packets algebraic methodology and software technology. ,vol. 100, pp. 536- 550 ,(1996) , 10.1007/BFB0014338
Robin Milner, Communication and Concurrency ,(1989)
Rance Cleaveland, Steve Sims, The NCSU Concurrency Workbench computer aided verification. pp. 394- 397 ,(1996) , 10.1007/3-540-61474-5_87
Julian Bradfield, Colin Stirling, Verifying temporal properties of processes international conference on concurrency theory. pp. 115- 125 ,(1990) , 10.1007/BFB0039055
Glenn Bruns, A Case Study in Safety-Critical Design computer aided verification. pp. 220- 233 ,(1992) , 10.1007/3-540-56496-9_18
Glenn Bruns, A Practical Technique for Process Abstraction international conference on concurrency theory. pp. 37- 49 ,(1993) , 10.1007/3-540-57208-2_4
Antonella Santone, Nicoletta De Francesco, Gigliola Vaglini, Roberto Barbuti, Selective mu-calculus: New modal operators for proving properties on reduced transition systems Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE). pp. 519- 534 ,(1997)
Claude Jard, Thierry Jéron, Bounded-memory Algorithms for Verification On-the-fly computer aided verification. pp. 192- 202 ,(1991) , 10.1007/3-540-55179-4_19