Abstract
Integrated formal specifications are intrinsically difficult to (automatically) verify due to the combination of complex data and behaviour. In this paper, we present a method for decomposing specifications into several smaller parts which can be independently verified. Verification results can then be combined to make a global result according to the original specification.
Instead of relying on an a priori given structure of the system such as a parallel composition of components, we compute the decomposition by ourselves using the technique of slicing. With less effort, significant properties can be verified for the resulting specification parts and be applied to the full specification. We prove correctness of our method and exemplify it according to a specification from the rail domain.
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
Brückner, I., Metzler, B., Wehrheim, H.: Optimizing slicing of formal specifications by deductive verification. Nordic Journal of Computing 13(1–2), 22–45 (2006)
Brückner, I., Wehrheim, H.: Slicing an Integrated Formal Method for Verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 360–374. Springer, Heidelberg (2005)
Brückner, I., Wehrheim, H.: Slicing Object-Z Specifications for Verification. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 414–433. Springer, Heidelberg (2005)
Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2(3), 279–287 (1999)
de Roever, W.P., Hanneman, U., Hooiman, J., Lakhneche, Y., Poel, M., Zwiers, J., de Boer, F.: Concurrency Verification. Cambridge University Press, Cambridge, UK (2001)
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. Chapman & Hall, Sydney (1997)
Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: IFM, pp. 315–334 (1999)
Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing Software for Model Construction. Higher-Order and Symbolic Computation 13(4), 315–353 (2000)
Hoare, C.A.R.: Communicating Sequential Processes. CACM 21, 666–677 (1978)
Kupferman, O., Vardi, M.Y.: Modular model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 381–401. Springer, Heidelberg (1998)
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, Berlin Heidelberg (1995)
Mota, A., Sampaio, A.: Model-checking CSP-Z. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 205–220. Springer, Heidelberg (1998)
Roscoe, A.W.: Model-checking csp. pp. 353–378 (1994)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Schneider, S., Treharne, H.: Verifying controlled components. IFM, pp. 87–107 (2004)
Smith, G. (ed.): The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)
Smith, G., Wildman, L.: Model checking Z specifications using SAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 85–103. Springer, Heidelberg (2005)
Wehrheim, H.: Incremental slicing. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 514–528. Springer, Heidelberg (2006)
Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Computer Society Press, Los Alamitos (1981)
Woodcock, J., Davies, J.: Using Z – Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Metzler, B. (2007). Decomposing Integrated Specifications for Verification. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)