Model fusion for the compatibility verification of software components
Zuberek, W.M.
in Proc. of the Ninth IEEE Int. Conf. on Dependability of Computer
Systems (DEPCOS14), Brunow Palace, Poland, June 30  July 4, 2014,
Springer Int. Publ. Switzerland 2014, pp.521529.
Abstract:
Similarly as in earlier work on component compatibility, the behavior of
components is specified by component interface languages, defined by
labeled Petri nets. In the case of composition of concurrent components,
the requests from different components can be interleaved, and  as shown
earlier  such interleaving can result in deadlocks in the composed system
even if each pair of interacting components is deadlockfree. Therefore
the elements of a componentbased system are considered compatible only
if the composition is deadlockfree. This paper formally defines model
fusion, which is a composition of net models of individual components that
represents the interleaving of interface languages of interacting components.
It also shows that the verification of component compatibility can avoid
the exhaustive analysis of the composed state space.
Keywords:
software components, componentbased systems, component composition,
component compatibility, compatibility verification, model fusion,
labelled Petri nets
References:

C. Attiogbe, P.Andre, G. Ardourel, "Checking component composability";
Proc. 5th Int. Symp. on Software Composition (Lecture Notes in Computer
Science 4089), pp.1833, 2006.

C. Baier, J. Klein, S. Klueppenholz, "Modeling and verification of components
and connectors"; in Formal Methods for Eternal Networked Software
Systems (Lecture Notes in Computer Science 6659), pp.114147, 2011.

E.T. Boer, T. Murata, "Generating basis siphons and traps of Petri nets
using the sign incidence matrix"; IEEE Trans. on Circuits and Systems,
I  Fundamental Theory and Applications, vol.41, no.4, pp.266271, 1994.

M. Broy, "A theory of system interaction: components, interfaces, and
services"; in Interactive Computations: The New Paradigm,
SpringerVerlag, pp.4196, 2006.

S. Chaki, S.M. Clarke, A. Groce, S. Jha, H. Veith, "Modular verification
of software components in C"; IEEE Trans. on Software Engineering, vol.30,
no.6, pp.388402, 2004.

F. Chu, X. Xie, "Deadlock analysis of Petri nets using siphons and
mathematical programming"; IEEE Trans. on Robotics and Automation,
vol.13, no.6, pp.793804, 1997.

D.C. Craig, W.M. Zuberek, "Compatibility of software
components  modeling and verification"; Proc. Int. Conf. on Dependability
of Computer Systems, Szklarska Poreba, Poland, pp.1118, 2006.

D.C. Craig, W.M. Zuberek, "Petri nets in modeling
component behavior and verifying component compatibility"; Proc. Int.
Workshop on Petri Nets and Software Engineering, Siedlce, Poland, pp.160174,
2007.

I. Crnkovic, H.W. Schmidt, J. Stafford, K. Wallnau, "Automated componentbased
software engineering"; The Journal of Systems and Software, vol.74, no.1,
pp.13, 2005.

D. Garlan, "Formal modeling and analysis of software architecture: components,
connectors and events"; Proc. Third Int. School on Formal Methods for the
Design of Computer, Communication and Software Systems: Software Architectures
(SFM 2003) (Lecture Notes in Computer Science 2804), pp.124, 2003.

L. Henrio, F. Kammueller, M.U. Khan, "A framework for reasoning on component
composition"; Proc. 8th Int. Symp. on Formal Methods for Components and
Objects (Lecture Notes in Computer Science 6286), pp.4169, 2009.

J.E. Hopcroft, R. Motwani, J.D. Ullman, Introduction to automata theory,
languages, and computations (2 ed.); AddisonWesley 2001.

A. Leicher, S. Busse, J.G. Suess, "Analysis of compositional conflicts in
componentbased systems"; Proc. 4th Int. Workshop on Software Composition;
Edinburgh, UK (Lecture Notes in Computer Science 3628), pp.6782, 2005.

T. Murata, "Petri nets: properties, analysis, and applications"; Proceedings
of the IEEE, vol.77, no.4, pp.541580, 1989.

W. Reisig, Petri nets  an introduction (EATCS Monographs on
Theoretical Computer Science 4); SpringerVerlag 1985.

W. Reisig,Understanding Petri nets  modeling techniques, analysis
methods, case studies; SpringerVerlag 2013.
% ISBN 9783642332777.

C. Szyperski, Component software: beyond objectoriented programming
(2 ed.); AddisonWesley Professional 2002.

A.M. Zaremski, J.M. Wang, "Specification matching of software components";
ACM Trans. on Software Engineering and Methodology, vol.6, no.4, pp.333369,
1997.

W.M. Zuberek, "Siphonbased verification of
component compatibility"; Proc. 4th Int. Conference on Dependability
of Computer Systems (DepCoS09); Brunow Palace, Poland, pp.123132, 2009.

W.M. Zuberek, "Checking compatibility and
substitutability of software components"; in Models and Methodology
of System Dependability; Oficyna Wydawnicza Politechniki Wroclawskiej,
ch.14, pp.175186, 2010.

W.M. Zuberek, "Incremental composition of software
components"a; in Dependable Computer Systems (Advances in
Intelligent and Soft Computing 97), SpringerVerlag, pp.301311, 2011.

W.M. Zuberek, "Service renaming in component.
composition; in: Complex Systems and Dependability (Advances
in Intelligent and Soft Computing 170), SpringerVerlag, pp.319330, 2012.
Available in pdf.