Abstract
The language Csp-Casl combines specifications of data and processes. We give an institution based semantics to Csp-Casl that allows us to re-use the institution independent structuring mechanisms of Casl. Furthermore, we extend Csp-Casl with a notion of refinement that reconciles the differing philosophies behind the refinement notions for Csp and Casl. We develop a compositional proof calculus for refinement along the Casl structuring mechanisms, and demonstrate that compositional proof techniques along parallel process composition from the context of Csp lifts to structured Csp-Casl specifications.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
eft/pos 2000 Specification, version 1.0.1. EP2 Consortium (2002)
Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)
Bidoit, M., Cengarle, V.V., Hennicker, R.: Proof systems for structured specifications and their refinements. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Fondations of System Specification, pp. 385–434. Springer, Heidelberg (1999)
Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)
Cerioli, M., Meseguer, J.: May I borrow your logic (Transporting logical structures along maps). Theoretical Computer Science 173, 311–347 (1997)
Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Logical Environments, Cambridge, pp. 83–130 (1993)
Fischer, C.: How to Combine Z with a Process Algebra. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 5–25. Springer, Heidelberg (1998)
Gimblett, A., Roggenbach, M., Schlingloff, B.-H.: Towards a Formal Specification of an Electronic Payment System in CSP-CASL. In: Fiadeiro, J.L., Mosses, P.D., Yu, Y. (eds.) WADT 2004. LNCS, vol. 3423, pp. 61–78. Springer, Heidelberg (2005)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)
Kahsai, T., Roggenbach, M.: Property Preserving Refinement for Csp-Casl. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 206–220. Springer, Heidelberg (2009)
Mossakowski, T.: ModalCASL. Language Summary (2004), http://www.informatik.uni-bremen.de/~till/papers/Modal-Summary.pdf
Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
Mossakowski, T., Roggenbach, M.: Structured CSP – A Process Algebra as an Institution. In: Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol. 4409, pp. 92–110. Springer, Heidelberg (2007)
Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)
O’Reilly, L., Kahsai, T., Mossakowski, T., Roggenbach, M.: The CSP-CASL institution. Technical Report CSR-1-2011, Swansea University (2011)
O’Reilly, L., Roggenbach, M., Isobe, Y.: CSP-CASL-Prover: A generic tool for process and data refinement. ENTCS 250(2), 69–84 (2009)
Reed, J.N., Sinclair, J.E., Roscoe, A.W.: Responsiveness of interoperating components. Formal Asp. Comput. 16(4), 394–411 (2004)
Reggio, G., Astesiano, E., Choppy, C.: Casl-LTL. Technical Report DISI-TR-99-34, Università di Genova (2000)
Roggenbach, M.: CSP-CASL: A new integration of process algebra and algebraic specification. Theoretical Computer Science 354(1), 42–71 (2006)
Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010)
Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)
Scattergood, B.: The semantics and implementation of machine-readable CSP. PhD thesis, Oxford University (1998)
Wehrheim, H.: Behavioural subtyping in object-oriented specification formalisms, Habilitation thesis, Carl-von-Ossietzky-Universität Oldenburg (2002)
Zawłocki, A.: Architectural Specifications for Reactive Systems. In: Fiadeiro, J.L., Mosses, P.D., Yu, Y. (eds.) WADT 2004. LNCS, vol. 3423, pp. 252–269. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
O’Reilly, L., Mossakowski, T., Roggenbach, M. (2012). Compositional Modelling and Reasoning in an Institution for Processes and Data. In: Mossakowski, T., Kreowski, HJ. (eds) Recent Trends in Algebraic Development Techniques. WADT 2010. Lecture Notes in Computer Science, vol 7137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28412-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-28412-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28411-3
Online ISBN: 978-3-642-28412-0
eBook Packages: Computer ScienceComputer Science (R0)