SEQ.OPEN: A tool for efficient trace-based verification

作者: Hubert Garavel , Radu Mateescu

DOI: 10.1007/978-3-540-24732-6_11

关键词:

摘要: We report about recent enhancements of the Cadp verification tool set that allow to check correctness event traces obtained by simulating or executing complex, industrial-size systems. Correctness properties are expressed using either regular expressions modal μ-calculus formulas, and verified efficiently on very large traces.

参考文章(18)
E. Allen Emerson, Chin Laung Lei, EFFICIENT MODEL CHECKING IN FRAGMENTS OF THE PROPOSITIONAL MU-CALCULUS. logic in computer science. pp. 267- 278 ,(1986)
Grigore Rosu, Klaus Havelund, Allen Goldberg, Dennis Koga, Robert Filman, Program Instrumentation and Trace Analysis ,(2002)
Hubert Garavel, OPEN/CÆSAR: An OPen Software Architecture for Verification, Simulation, and Testing tools and algorithms for construction and analysis of systems. pp. 68- 84 ,(1998) , 10.1007/BFB0054165
Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, MosheY. Vardi, Yael Zbar, The ForSpec Temporal Logic: A New Temporal Property-Specification Language tools and algorithms for construction and analysis of systems. pp. 296- 311 ,(2002) , 10.1007/3-540-46002-0_21
Radu Mateescu, A generic on-the-fly solver for alternation-free boolean equation systems tools and algorithms for construction and analysis of systems. pp. 81- 96 ,(2003) , 10.1007/3-540-36577-X_7
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Hubert Garavel, Radu Mateescu, Frédéric Lang, An overview of CADP 2001 INRIA. pp. 15- ,(2001)
Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh, The Temporal Logic Sugar computer aided verification. pp. 363- 367 ,(2001) , 10.1007/3-540-44585-4_33
Rocco Nicola, Frits Vaandrager, Action versus state based logics for transition systems Semantics of Systems of Concurrent Processes. pp. 407- 419 ,(1990) , 10.1007/3-540-53479-2_17