Abstract
Infinite models cannot be directly analyzed by model checking. An alternative for achieving that is using data abstraction to derive a simpler (abstract) but finite model so that the properties can be verified using the abstract model instead. This work proposes a strategy and an algorithm for generating abstractions of systems modeled in the process algebra CSP. These abstractions are safe in the sense that they preserve trace-based refinements. We show the application of our strategy to an example.
This is a preview of subscription content, log in via an institution to check access.
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
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. ACM SIGPLAN Notices 36(5), 203–213 (2001)
Bourdoncle, F.: Abstract interpretation by dynamic partitioning. Journal of Functional Programming 2(04), 407–435 (2008)
Bryant, R.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR) 24(3), 293–318 (1992)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. Informatics-10 Years Back 10, 176–194 (2001)
Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. Journal of Logic and Computation 2(4), 511–547 (2004)
Farias, A., Mota, A., Sampaio, A.: Efficient CSP-Z Data Abstraction. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 108–127. Springer, Heidelberg (2004)
Farias, A., Mota, A., Sampaio, A.: Compositional abstraction of CSP-Z processes. Journal of the Brazilian Computer Society 14, 23–44 (2008)
Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol. 2, pp. 423–438 (1997)
Forjaz, M.: The origins of Embraer. Tempo Social 17, 281–298 (2005)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Lazic, R., Roscoe, A.: A semantic study of data independence with applications to model checking. Bulletin-European Association For Theoretical Computer Science 71, 259–260 (2000)
Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1998)
Sampaio, A., Albuquerque, C., Vasconcelos, J., Cruz, L., Figueiredo, L., Cavalcante, S.: Software test program: a software residency experience. In: ICSE 2005: Proceedings of the 27th international conference on Software engineering, pp. 611–612. ACM Press, New York (2005)
Smith, G.: The Object-Z Specification Language. Springer, Heidelberg (2000)
Systems, F.: Failures-Divergence Refinement - FDR2 User Manual, June 2005. Formal Systems (Europe) Ltd. (June 2005)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering 10(2), 203–232 (2003)
Wehrheim, H.: Data Abstraction Techniques in the Validation of CSP-OZ Specifications. Formal Aspects of Computing 12(3), 147–164 (2000)
Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River (1996)
Yorav, S., Clarke, E.: Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. Electronic Notes in Theoretical Computer Science 89(3), 105–127 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damasceno, A., Farias, A., Mota, A. (2009). A Mechanized Strategy for Safe Abstraction of CSP Specifications. In: Oliveira, M.V.M., Woodcock, J. (eds) Formal Methods: Foundations and Applications. SBMF 2009. Lecture Notes in Computer Science, vol 5902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10452-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-10452-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10451-0
Online ISBN: 978-3-642-10452-7
eBook Packages: Computer ScienceComputer Science (R0)