Abstract
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying certain temporal properties. To remedy this problem, we show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for in finite state systems, and shed light on the relationship between “classical” model checking and refinement checking.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.-R. Abrial. The B-Book. Cambridge University Press, 1996.
B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, October 1985.
A. Pnueli. The temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.
R. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
M. Butler and C. Morgan. Action systems, unbounded nondeterminism, and infinite traces. Formal Aspects of Computing, 7:37–53, 1995.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626–643, Dec. 1996.
S. J. Creese and A. W. Roscoe. Data independent induction over structured networks. In International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA’ 00), Las Vegas, USA, June 2000.
M. Leuschel, T. Massart, and A. Currie. How to make FDR spin: LTL model checking of CSP by refinement. Technical Report DSSE-TR-2000-10, Department of Electronics and Computer Science, University of Southampton, September 2000.
J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.
Formal Systems (Europe) Ltd. Failures-Divergence Refinement — FDR2 User Manual.
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Workshop on Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.
C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
M. Leuschel and T. Massart. In_nite state model checking by abstract interpretation and program specialisation. In A. Bossi, editor, Proceedings of LOPSTR’99, LNCS 1817, pages 63–82, Venice, Italy, September 1999.
J. Magee and J. Kramer. Concurrency: State Models & Java Programs. Wiley, 1999.
K. L. McMillan. Symbolic Model Checking. PhD thesis, Boston, 1993.
A. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997.
A. W. Roscoe and R. S. Lazic. Using logical relations for automated verification of data-independent CSP. In Proceedings of Oxford Workshop on Automated Formal Methods ENTCS, 1996.
R. Sedgewick. Algorithms in C++. Addison-Wesley, 1992.
A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733–749, July 1985.
A. Valmari. On-the-fly veri_cation with stubborn sets. In C. Courcoubetis, editor, Proceedings of CAV’93, LNCS 697, pages 397–408. Springer-Verlag, 1993.
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of LICS’86, pages 332–344, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leuschel, M., Currie, A., Massart, T. (2001). How to Make FDR Spin LTL Model Checking of CSP by Refinement. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_6
Download citation
DOI: https://doi.org/10.1007/3-540-45251-6_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41791-0
Online ISBN: 978-3-540-45251-5
eBook Packages: Springer Book Archive