Abstract
A concurrent object system is a dynamically growing collection of concurrently interacting objects. Such a system is called open if the environment of the system is unknown. Proving properties about open systems is challenging because the properties must be shown to hold for all possible environments of the system. Hierarchical reasoning, which infers properties of large components from the properties of smaller subcomponents, is a key enabler to manage the reasoning effort.
This chapter presents an approach to hierarchically specify and verify open concurrent object systems. We introduce a core calculus for concurrent object systems. The behavior of such a system is given by a standard operational semantics. To abstract from the internal representation of the objects, we develop an alternative trace-based semantics that captures the behavior in terms of the communication traces between the objects of the system and the environment. The main advantage of the trace-based model is its extendability to components and open systems while remaining faithful to the operational model. The specification approach is also directly based on the traces and supports hierarchical reasoning using the following two central features. Looseness allows specification refinement. Restriction allows expressing assumptions on the environment. Finally, we provide a Hoare-style proof system that handles the given specifications.
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.
This work is partially supported by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using Formal Models.
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
Ábrahám-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for Java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 5–20. Springer, Heidelberg (2002)
Ábrahám, E., Grabe, I., Grüner, A., Steffen, M.: Behavioral interface description of an object-oriented language with futures and promises. J. Log. Algebr. Program. 78(7), 491–518 (2009)
Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)
Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7(1), 1–72 (1997)
Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012)
Armstrong, J.: Erlang. Commun. ACM 53, 68–75 (2010)
Arts, T., Dam, M.: Verifying a distributed database lookup manager written in Erlang. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 682–700. Springer, Heidelberg (1999)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Baker Jr., H.G., Hewitt, C.: The incremental garbage collection of processes. SIGART Bull., 55–59 (August 1977)
de Boer, F.S.: A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theor. Comput. Sci. 274(1-2), 3–41 (2002)
de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)
Broy, M., Stølen, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, New York (2001)
Cardelli, L.: Class-based vs. object-based languages. PLDI Tutorial (1996)
Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: An event-based structural operational semantics of multi-threaded Java. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 157–200. Springer, Heidelberg (1999)
Clarke, D., Östlund, J., Sergey, I., Wrigstad, T.: Ownership types: A survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol. 7850, pp. 15–58. Springer, Heidelberg (2013)
Clinger, W.D.: Foundations of Actor Semantics. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA (1981)
Dam, M., Fredlund, L.-Å., Gurov, D.: Toward parametric verification of open distributed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 150–185. Springer, Heidelberg (1998)
Darlington, J., Guo, Y.: Formalising actors in linear logic. In: OOIS, pp. 37–53 (1994)
De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984)
Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: Component reasoning for concurrent objects. J. Log. Algebr. Program. 81(3), 227–256 (2012)
Din, C.C., Dovland, J., Owe, O.: An approach to compositional reasoning about concurrent objects and futures. Research Report 415 (2012)
Din, C.C., Dovland, J., Owe, O.: Compositional reasoning about shared futures. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 94–108. Springer, Heidelberg (2012)
Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: SwSTE, pp. 141–150. IEEE Computer Society (2005)
Duarte, C.H.C.: Proof-Theoretic foundations for the design of actor systems. Mathematical Structures in Computer Science 9(3), 227–252 (1999)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Longman Publishing Co., Inc., Boston (1995)
Gusfield, D.: Algorithms on Strings, Trees, and Sequences - Computer Science and Computational Biology. Cambridge University Press (1997)
Hähnle, R.: The Abstract Behavioral Specification language: A tutorial introduction. In: de Boer, F., Bonsangue, M., Giachino, E., Hähnle, R. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 1–37. Springer, Heidelberg (2013)
Haller, P.: On the integration of the actor model in mainstream technologies: The Scala perspective. In: AGERE! 2012, pp. 1–6. ACM, New York (2012)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
International Telecommunication Union: Open distributed processing – reference models parts 1–4. Tech. rep., ISO/IEC (1995)
Johnsen, E.B., Blanchette, J.C., Kyas, M., Owe, O.: Intra-Object versus Inter-Object: Concurrency and reasoning in Creol. Electr. Notes Theor. Comput. Sci. 243, 89–103 (2009)
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)
Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theor. Comput. Sci. 365(1-2), 23–66 (2006)
Jonsson, B.: A fully abstract trace model for dataflow and asynchronous networks. Distributed Computing 7(4), 197–212 (1994)
Kahn, G.: The semantics of simple language for parallel programming. In: IFIP Congress, pp. 471–475 (1974)
Kurnia, I.W., Poetzsch-Heffter, A.: A relational trace logic for simple hierarchical actor-based component systems. In: AGERE! 2012, pp. 47–58. ACM, New York (2012), http://doi.acm.org/10.1145/2414639.2414647
Lamport, L., Schneider, F.B.: The “Hoare logic” of CSP, and all that. ACM Trans. Program. Lang. Syst. 6(2), 281–296 (1984), http://doi.acm.org/10.1145/2993.357247
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)
Microsoft: Component Object Model (COM) (January 1999), http://www.microsoft.com/com/default.asp
Milner, R.: A Calculus of Communicating Systems. Springer-Verlag New York, Inc., Secaucus (1982)
Milner, R.: Communicating and Mobile Systems – The π-Calculus. Cambridge University Press (1999)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)
Nain, S., Vardi, M.Y.: Trace semantics is fully abstract. In: LICS, pp. 59–68. IEEE Computer Society (2009)
Olderog, E.R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM Trans. Program. Lang. Syst. 10(3), 420–455 (1988)
OMG: CORBA component model v4.0 (2006), http://www.omg.org/spec/CCM/
Philippsen, M.: A survey of concurrent object-oriented languages. Concurrency - Practice and Experience 12(10), 917–980 (2000)
Poetzsch-Heffter, A., Feller, C., Kurnia, I.W., Welsch, Y.: Model-based compatibility checking of system modifications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 97–111. Springer, Heidelberg (2012)
de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press (2001)
Roth, A.: Specification and Verification of Object-Oriented Software Components. Ph.D. thesis, University of Karlsruhe (2006)
Sangiorgi, D., Walker, D.: The Pi-Calculus – A Theory of Mobile Processes. Cambridge University Press (2001)
Schacht, S.: Formal reasoning about actor programs using temporal logic. In: Agha, G., De Cindio, F., Rozenberg, G. (eds.) APN 2001. LNCS, vol. 2001, pp. 445–460. Springer, Heidelberg (2001)
Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275–299. Springer, Heidelberg (2010)
Smith, S.F., Talcott, C.L.: Specification diagrams for actor systems. Higher-Order and Symbolic Computation 15(4), 301–348 (2002)
Soundarajan, N.: A proof technique for parallel programs. Theoretical Computer Science 31(1-2), 13–29 (1984)
Steffen, M.: Object-Connectivity and Observability for Class-Based, Object-Oriented Languages. Habilitation thesis, Technische Faktultät der Christian-Albrechts-Universität zu Kiel, 281 pages (Jul 2006)
Stirling, C.: An introduction to modal and temporal logics for CCS. In: Yonezawa, A., Ito, T. (eds.) UK/Japan WS 1989. LNCS, vol. 491, pp. 1–20. Springer, Heidelberg (1991)
Talcott, C.L.: Composable semantic models for actor theories. Higher-Order and Symbolic Computation 11(3), 281–343 (1998)
Thati, P., Talcott, C., Agha, G.: Techniques for executing and reasoning about specification diagrams. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 521–536. Springer, Heidelberg (2004)
The OSGi Alliance: OSGi core release 5 (2012), http://www.osgi.org
Vasconcelos, V.T., Tokoro, M.: Traces semantics for actor systems. In: Zatarain-Cabada, R., Wang, J. (eds.) ECOOP-WS 1991. LNCS, vol. 612, pp. 141–162. Springer, Heidelberg (1992)
Widom, J., Gries, D., Schneider, F.B.: Completeness and incompleteness of trace-based network proof systems. In: POPL, pp. 27–38 (1987)
Yonezawa, A., Briot, J.P., Shibayama, E.: Object-oriented concurrent programming in ABCL/1. In: OOPSLA, pp. 258–268 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kurnia, I.W., Poetzsch-Heffter, A. (2013). Verification of Open Concurrent Object Systems. In: Giachino, E., Hähnle, R., de Boer, F.S., Bonsangue, M.M. (eds) Formal Methods for Components and Objects. FMCO 2012. Lecture Notes in Computer Science, vol 7866. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40615-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-40615-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40614-0
Online ISBN: 978-3-642-40615-7
eBook Packages: Computer ScienceComputer Science (R0)