Behavioural semantics for asynchronous components. (English) Zbl 1407.68271

Summary: Software components are a valuable programming abstraction that enables a compositional design of complex applications. In distributed systems, components can also be used to provide an abstraction of locations: each component is a unit of deployment that can be placed on a different machine. In this article, we consider this kind of distributed components that are additionally loosely coupled and communicate by asynchronous invocations.
Components also provide a convenient abstraction for verifying the correct behaviour of systems: they provide structuring entities easing the correctness verification. This article provides a formal background for the generation of behavioural semantics for asynchronous components. It expresses the semantics of hierarchical distributed components communicating asynchronously by requests, futures, and replies; this semantics is provided using the pNet intermediate language. This article both demonstrates the expressiveness of the pNet model and formally specifies the complete process of the generation of a behavioural model for a distributed component system. The purpose of our behavioural semantics is to allow for verification both by finite instantiation and model-checking, and by techniques for infinite systems.


68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI HAL


[1] The common component architecture (CCA) forum home page, (2005)
[2] CORBA component model specification, (April 2006), OMG Headquarters edition
[3] Beisiegel, M.; Blohm, H.; Booz, D.; Edwards, M.; Hurley, O., SCA service component architecture, assembly model specification, (March 2007), OSOA, Tech. rep
[4] Baude, F.; Caromel, D.; Dalmasso, C.; Danelutto, M.; Getov, V.; Henrio, L.; Pérez, C., GCM: a grid extension to fractal for autonomous distributed components, Ann. Télécommun., 64, 1-2, 5-24, (2009)
[5] Barros, T.; Ameur-Boulifa, R.; Cansado, A.; Henrio, L.; Madelaine, E., Behavioural models for distributed fractal components, Ann. Télécommun., 64, 1-2, 25-43, (2009)
[6] Henrio, L.; Madelaine, E.; Zhang, M., A theory for the composition of concurrent processes, (Albert, E.; Lanese, I., 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Formal Techniques for Distributed Objects, Components, and Systems, Heraklion, Greece, LNCS, vol. 9688, (2016)), 175-194 · Zbl 1347.68267
[7] Barros, T.; Henrio, L.; Madelaine, E., Verification of distributed hierarchical components, (International Workshop on Formal Aspects of Component Software (FACS’05), Macao, Electronic Notes in Theoretical Computer Science (ENTCS), (2005))
[8] Cansado, A.; Henrio, L.; Madelaine, E., Transparent first-class futures and distributed component, (International Workshop on Formal Aspects of Component Software (FACS’08), Malaga, (2008))
[9] Ameur-Boulifa, R.; Halalai, R.; Henrio, L.; Madelaine, E., Verifying safety of fault-tolerant distributed components, (International Workshop on Formal Aspects of Component Software (FACS’11), Oslo, (2011))
[10] Kulankhina, O., A framework for rigorous development of distributed components: formalisation and tools, (Octobre 2016), Université de Nice Sophia Antipolis, Ph.D. thesis
[11] Gaspar, N.; Henrio, L.; Madelaine, E., Formally reasoning on a reconfigurable component-based system - a case study for the industrial world, (International Symposium on Formal Aspects of Component Software (FACS 2013), Nanchang, China, Lecture Notes in Computer Science, (2013), Springer)
[12] Boulifa, R. A.; Henrio, L.; Madelaine, E., Behavioural models for group communications, (WCSI-10: International Workshop on Component and Service Interoperability, Malaga, Spain, (2010))
[13] Henrio, L.; Kammüller, F.; Rivera, M., An asynchronous distributed component model and its semantics, (de Boer, F.; Bonsangue, M.; Madelaine, E., FMCO’08, LNCS, vol. 5751, (2008), Springer Heidelberg), 159-179
[14] Henrio, L.; Kammüller, F.; Khan, M. U., A framework for reasoning on component composition, (FMCO 2009, Lecture Notes in Computer Science, (2010), Springer)
[15] Bruneton, E.; Coupaye, T.; Leclerc, M.; Quéma, V.; Stefani, J.-B., The fractal component model and its support in Java, Softw. Pract. Exp., 36, 11-12, (2006), special issue on Experiences with Auto-adaptive and Reconfigurable Systems
[16] Johnsen, E. B.; Owe, O.; Yu, I. C., Creol: a types-safe object-oriented model for distributed concurrent systems, J. Theor. Comput. Sci., 365, 1-2, 23-66, (2006) · Zbl 1118.68031
[17] Dedecker, J.; Cutsem, T. V.; Mostinckx, S.; D’Hondt, T.; Meuter, W. D., Ambient-oriented programming in ambienttalk, (Thomas, D., ECOOP, Lecture Notes in Computer Science, vol. 4067, (2006), Springer), 230-254
[18] Schäfer, J.; Poetzsch-Heffter, A., Jcobox: generalizing active objects to concurrent components, (ECOOP 2010 - Object-Oriented Programming, (2010)), 275-299
[19] Johnsen, E.; Hähnle, R.; Schäfer, J.; Schlatte, R.; Steffen, M., ABS: a core language for abstract behavioral specification, (Formal Methods for Components and Objects, LNCS, vol. 6957, (2012), Springer Berlin, Heidelberg), 142-164
[20] Ziaei, R.; Agha, G., Synchnet: a Petri net based coordination language for distributed objects, (Pfenning, F.; Smaragdakis, Y., GPCE, Lecture Notes in Computer Science, vol. 2830, (2003), Springer), 324-343
[21] Bruneton, E.; Coupaye, T.; Leclerc, M.; Quema, V.; Stefani, J. B., An open component model and its support in Java, (7th Int. Symp. on Component-Based Software Engineering (CBSE-7), LNCS, vol. 3054, (2004))
[22] Bruneton, E.; Coupaye, T.; Stefani, J. B., The fractal component model, (February 2004), ObjectWeb Consortium, Tech. rep.
[23] Agha, G.; Mason, I. A.; Smith, S. F.; Talcott, C. L., A foundation for actor computation, J. Funct. Program., 7, 1, 1-72, (1997) · Zbl 0870.68091
[24] Mattern, F.; Fünfrocken, S., A non-blocking lightweight implementation of causal order message delivery, (Birman, K. P.; Mattern, F.; Schiper, A., Theory and Practice in Distributed Systems: International Workshop Dagstuhl, Castle, Germany, September 5-9, 1994, Selected Papers, (1995), Springer Berlin, Heidelberg), 197-213
[25] Charron-Bost, B.; Mattern, F.; Tel, G., Synchronous, asynchronous, and causally ordered communications, Distrib. Comput., 9, 173-191, (1996)
[26] Varela, C. A., Programming distributed computing systems: A foundational approach, (2013), The MIT Press · Zbl 1275.68004
[27] Caromel, D.; Henrio, L.; Serpette, B., Asynchronous and deterministic objects, (Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (2004), ACM Press), 123-134 · Zbl 1325.68052
[28] Henrio, L., Formal models for programming and composing correct distributed systems, (Jul. 2012), Université de Nice Sophia-Antipolis, HDR Thesis
[29] Henrio, L.; Madelaine, E.; Zhang, M., Pnets: an expressive model for parameterised networks of processes, (Formal Approaches to Parallel and Distributed Systems (4PAD) - Special Session of Parallel, Distributed and Network-Based Processing (PDP), Turku, Finland, (2015)), extended version in
[30] Cleaveland, R.; Riely, J., Testing-based abstractions for value-passing systems, (Jonsson, J. P.B., Int. Conf. on Concurrency Theory (CONCUR’94), LNCS, vol. 836, (1994), Springer Heidelberg), 417-432
[31] Henrio, L.; Kulankhina, O.; Madelaine, E., Integrated environment for verifying and running distributed components, (Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2016), LNCS, (2016), Springer Berlin, Heidelberg), 66-83
[32] Caromel, D.; Henrio, L., A theory of distributed objects, (2005), Springer-Verlag New York · Zbl 1084.68012
[33] Mason, I. A.; Talcott, C. L., Actor languages their syntax, semantics, translation, and equivalence, Theor. Comput. Sci., 220, 2, 409-467, (1999) · Zbl 0954.68089
[34] Dam, M.; Palmskog, K., Location-independent routing in process network overlays, Serv. Oriented Comput. Appl., 9, 3-4, 285-309, (2015)
[35] Henrio, L.; Khan, M. U., Asynchronous components with futures: semantics and proofs in isabelle/hol, (Proceedings of the Seventh International Workshop, FESCA 2010, ENTCS, (2010))
[36] Henrio, L.; Kulankhina, O.; Liu, D.; Madelaine, E., Verifying the correct composition of distributed components: formalisation and tool, (FOCLASA, Rome, Italy, (2014))
[37] Garavel, H.; Lang, F.; Mateescu, R., An overview of CADP 2001, Eur. Assoc. Softw. Sci. Technol. Newsl., 4, 13-24, (2002)
[38] Mateescu, R.; Thivolle, D., A model checking language for concurrent value-passing systems, (Cuellar, K. S.J.; Maibaum, T. S.E., FM’08, LNCS, vol. 5014, (2008), Springer Heidelberg)
[39] Garlan, D.; Monroe, R. T.; Wile, D., Acme: architectural description of component-based systems, (Foundations of Component-Based Systems, (2000)), 47-68
[40] Bures, T.; Hnetynka, P.; Plasil, F., SOFA 2.0: balancing advanced features in a hierarchical component model, (Proceedings of SERA 2006, (2006), IEEE CS), 40-48
[41] Ameur-Boulifa, R.; Henrio, L.; Madelaine, E.; Savu, A., Behavioural semantics for asynchronous components, (Dec. 2012), INRIA, Research Report RR-8167 · Zbl 1407.68271
[42] Eker, J.; Janneck, J. W.; Lee, E. A.; Liu, J.; Liu, X.; Ludvig, J.; Neuendorffer, S.; Sachs, S. R.; Xiong, Y., Taming heterogeneity - the Ptolemy approach, Proc. IEEE, 91, 1, 127-144, (2003)
[43] Aldinucci, M.; Bertolli, C.; Campa, S.; Coppola, M.; Vanneschi, M.; Zoccolo, C., Autonomic grid components: the GCM proposal and self-optimising ASSIST components, (Joint Workshop on HPC Grid Programming Environments and Components and Component and Framework Technology in High-Performance and Scientific Computing at HPDC’15, (2006))
[44] Merle, P.; Stefani, J.-B., A formal specification of the fractal component model in alloy, (2008), INRIA, Research Report RR-6721
[45] de Boer, F. S.; Clarke, D.; Johnsen, E. B., A complete guide to the future, (De Nicola, R., Programming Languages and Systems, Lecture Notes in Computer Science, vol. 4421, (2007), Springer Berlin, Heidelberg), 316-330
[46] Plasil, F.; Visnovsky, S., Behavior protocols for software components, IEEE Trans. Softw. Eng., 28, 11, 1056-1076, (2002)
[47] Poch, T.; Sery, O.; Plasil, F.; Kofron, J., Threaded behavior protocols, Form. Asp. Comput., 25, 4, 543-572, (2013) · Zbl 1298.68066
[48] Kofron, J., Checking software component behavior using behavior protocols and spin, (Proceedings of Applied Computing 2007, Seoul, Korea, (2007))
[49] André, P.; Ardourel, G.; Attiogbé, C., Adaptation for hierarchical components and services, Electron. Notes Theor. Comput. Sci., 189, 5-20, (2007)
[50] Attiogbé, C.; André, P.; Ardourel, G., Checking component composability, (5th International Symposium on Software Composition (ETAPS/SC’06), Lecture Notes in Computer Science, vol. 4089, (2006), Springer Verlag)
[51] André, P.; Ardourel, G.; Attiogbé, C., Composing components with shared services in the kmelia model, (7th International Symposium on Software Composition, SC’08, LNCS, vol. 4954, (2008), Springer)
[52] Fernandes, F.; Royer, J.-C., The stslib project: towards a formal component model based on STS, Electron. Notes Theor. Comput. Sci., 215, 131-149, (2008)
[53] Bensalem, S.; Bozga, M.; Nguyen, T.-H.; Sifakis, J., Compositional verification for component-based systems and application, IET Softw., 4, 3, 181-193, (2010)
[54] Basu, A.; Bensalem, B.; Bozga, M.; Combaz, J.; Jaber, M.; Nguyen, T.-H.; Sifakis, J., Rigorous component-based system design using the BIP framework, IEEE Softw., 28, 3, 41-48, (2011)
[55] Bensalem, S.; Bozga, M.; Nguyen, T.-H.; Sifakis, J., D-finder: a tool for compositional deadlock detection and verification, (Computer Aided Verification, 21st International Conference, CAV 2009, Proceedings, Grenoble, France, June 26 - July 2, 2009, Lecture Notes in Computer Science, vol. 5643, (2009), Springer), 614-619
[56] Basu, A.; Gallien, M.; Lesire, C.; Nguyen, T.-H.; Bensalem, S.; Ingrand, F.; Sifakis, J., Incremental component-based construction and verification of a robotic system, (ECAI 2008 - 18th European Conference on Artificial Intelligence, Proceedings, Patras, Greece, July 21-25, 2008, Frontiers in Artificial Intelligence and Applications, vol. 178, (2008), IOS Press), 631-635
[57] Giachino, E.; Laneve, C.; Lienhardt, M., A framework for deadlock detection in ABS, J. Softw. Syst. Model., 1-36, (2015)
[58] Albert, E.; Arenas, P.; Flores-Montoya, A.; Genaim, S.; Gómez-Zamalloa, M.; Martin-Martin, E.; Puebla, G.; Román-Díez, G., SACO: static analyzer for concurrent objects, (Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 8413, (2014), Springer Berlin,Heidelberg), 562-567
[59] Din, C. C.; Bubel, R.; Hähnle, R., Key-ABS: a deductive verification tool for the concurrent modelling language ABS, (Proceedings of the 25th International Conference on Automated Deduction (CADE 2015), (2015), Springer), 517-526 · Zbl 1465.68174
[60] Sirjani, M.; de Boer, F. S.; Movaghar, A.; Shali, A., Extended rebeca: a component-based actor language with synchronous message passing, (Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 6-9 June 2005, St. Malo, France, (2005), IEEE Computer Society), 212-221
[61] Sirjani, M.; Movaghar, A.; Shali, A.; de Boer, F. S., Model checking, automated abstraction, and compositional verification of rebeca models, J. Univers. Comput. Sci., 11, 6, 1054-1082, (2005)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.