Abstract.
Component based design is a new methodology for the construction of distributed systems and applications. In this new setting, a system is built by the assembly of (pre)-existing components. Remains the problem of the compositional verification of such systems. We investigate methods and concepts for the provision of “sound” assemblies. We define an abstract, dynamic, multi-threaded, component model, encompassing both client/server and peer to peer communication patterns. We define a behavioural interface type language endowed with a (decidable) set of interface compatibilty rules. Based on the notion of compliance of components to their interfaces, we define the concepts of “contract” and “contract satisfaction”. This leads to the notion of sound assemblies of components, i.e., assemblies made of contracted components interacting through compatible interfaces. Sound assemblies possess interesting properties like “external deadlock freeness” and “message consumption”.
Chapter PDF
Similar content being viewed by others
References
Bailly, A.: Assume / Guarantee Contracts for Timed Mobile Objects. PhD thesis, ENST (December 2002)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE 2001, SOFTWARE ENGINEERING NOTES, vol. 26(5). ACM Press, New York (2001)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. INFCTRL: Information and Computation (formerly Information and Control) 173 (2002)
Kobayashi, N.: A type system for lock-free processes. INFCTRL: Information and Computation (formerly Information and Control) 177 (2002)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems 21(5) (1999)
Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition sytems. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019. Springer, Heidelberg (1995)
Nierstrasz, O.: Regular types for active objects. In: Object-Oriented Software Composition, pp. 99–121. Prentice-Hall, Englewood Cliffs (1995)
Najm, E., Nimour, A., Stefani, J.-B.: Guaranteeing liveness in an object calculus through behavioral typing. In: Proc. of FORTE/PSTV 1999 (October 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Carrez, C., Fantechi, A., Najm, E. (2003). Behavioural Contracts for a Sound Assembly of Components. In: König, H., Heiner, M., Wolisz, A. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2003. FORTE 2003. Lecture Notes in Computer Science, vol 2767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39979-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-39979-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20175-5
Online ISBN: 978-3-540-39979-7
eBook Packages: Springer Book Archive