Abstract
We introduce a new specification formalism which we call hiddenCCS; hidden algebra is used to specify local goals as objects, and CCS is used to describe global goal of the synchronizing concurrent objects. We extend the object specification with synchronization elements associated with methods of different objects, and we use a CCS coordinating module to describe the interaction patterns of methods invocations. Some results refer to strong bisimulation over the hiddenCCS configurations. We investigate how the existing tools BOBJ, CWB, and Maude can be integrated to describe and verify useful properties of the synchronizing concurrent objects. The hiddenCCS specifications can be described in the rewriting logic using Maude. Finally we present the first steps towards temporal specifications and verification for hiddenCCS.
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.
Similar content being viewed by others
References
Ciobanu, G., Lucanu, D.: Communicating Concurrent Objects in HiddenCCS. Accepted at WRLA 2004. To appear in Electronic Notes in Theoretical Computer Science, Elsevier (2004)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and Programming in Rewriting Logic Theoretical Computer Science, vol. 285(2), p. 187 (2002)
Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: a semantics-based tool for the verification of concurrent systems. In: ACM TOPLAS, vol. 15(1), pp. 36–72. ACM Press, New York (1993)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL Model Checker. In: Gadducci, F., Montanari, U. (eds.) 4th WRLA. Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, Amsterdam (2002)
Galloway, J., Stoddart, W.: An Operational Semantics for ZCCS. In: Hinchey, M.G., Liu, S. (eds.) Proc. ICFEM 1997, pp. 272–282. IEEE Computer Society Press, Los Alamitos (1997)
Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)
Goguen, J., Lin, K., Roşu, G.: Circular Coinductive Rewriting. In: Proc. Automated Software Engineering 2000, pp. 123–131. IEEE Press, Los Alamitos (2000)
Lucanu, D., Ciobanu, G.: Model Checking for Object Specifications in Hidden Algebra. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 97–109. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: Behavioral Membership Equational Logic. In: Proc. CMCS. Electronic Notes in Theoretical Computer Science, vol. 65, Elsevier, Amsterdam (2002)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press, Cambridge (1999)
Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)
Salaün, G., Allemand, M., Attiogbé, C.: A Formalism Combining CCS and CASL. RESEARCH REPORT No 00.14, IRIN, Université de Nantes (2001)
Taguchi, K., Araki, K.: The State-Based CCS Semantics for Concurrent Z Specification. In: Hinchey, M.G., Liu, S. (eds.) Proc. ICFEM 1997, pp. 283–292. IEEE Computer Society Press, Los Alamitos (1997)
Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude 2. In: Gadducci, F., Montanari, U. (eds.) Proc. WRLA. Electronic Notes in Theoretical Computer Science, vol. 71, pp. 239–257. Elsevier, Amsterdam (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciobanu, G., Lucanu, D. (2004). Specification and Verification of Synchronizing Concurrent Objects. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-24756-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21377-2
Online ISBN: 978-3-540-24756-2
eBook Packages: Springer Book Archive