摘要: We present a methodology for constructing abstractions and refining them by analyzing counter-examples. also uniform verification method that combines abstraction, model-checking deductive in novel way. In particular, it allows shows how to use the set of reachable states abstract system proof even when model does not satisfy specification simulates concrete with respect weaker simulation notion than Milner's.
core.ac.uk
springer.com
sci-hub.st 参考文章(34)
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems Springer New York. ,(1995) , 10.1007/978-1-4612-4222-2
Kai Baukus, Yassine Lakhnech, Karsten Stahl, Verifying Universal Properties of Parameterized Networks FTRTFT '00 Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. pp. 291- 303 ,(2000) , 10.1007/3-540-45352-0_24
Rance Cleaveland, Purush Iyer, Daniel Yankelevich, None, Optimality in Abstractions of Model Checking static analysis symposium. pp. 51- 63 ,(1995) , 10.1007/3-540-60360-3_32
Susanne Graf, Hassen Saidi, Construction of Abstract State Graphs with PVS computer aided verification. pp. 72- 83 ,(1997) , 10.1007/3-540-63166-6_10
Michael A. Colón, Tomás E. Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures computer aided verification. pp. 293- 304 ,(1998) , 10.1007/BFB0028753
A. Bouajjani, J-C. Fernandez, N. Halbwachs, Minimal Model Generation computer aided verification. pp. 197- 203 ,(1990) , 10.1007/BFB0023733
Felice Balarin, Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment computer aided verification. pp. 29- 40 ,(1993) , 10.1007/3-540-56922-7_4
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems: Safety ,(1995)
S. Bensalem, Y. Lakhnech, S. Owre, InVeST: A Tool for the Verification of Invariants computer aided verification. pp. 505- 510 ,(1998) , 10.1007/BFB0028771
Saddek Bensalem, Yassine Lakhnech, None, Automatic Generation of Invariants formal methods. ,vol. 15, pp. 75- 92 ,(1999) , 10.1023/A:1008744030390