Petri Nets in modeling component behavior and verifying component compatibility

Craig, D.C. and Zuberek, W.M.

Proc. Int. Workshop on Petri Nets and Software Engineering (PNSE'07), part of the 28-th Int. Conf. on Application and Theory of Petri Nets and Other Models of Councurrency, Siedlce, Poland, 25-26 June 2007, pp.160-174.

Abstract:

In component-based systems, two components are compatible if all possible sequences of services requested by one component can be provided by the other component. Verification of component compatibility is essential in large software systems as otherwise subtle software failures can exist which are difficult to detect through software testing. For verification of compatibility, the behavior of interacting components, at their interfaces, is modeled by labeled Petri nets with labels representing the requested and provided services, and such component models are composed. The composition operation is designed in such a way that component incompatibilities are manifested as deadlocks in the composed model. Compatibility verification is thus performed through deadlock detection in the composed models. Efficient structural techniques are proposed for deadlock analysis.

Keywords:

Software components, component-based systems, component compatibility, compatilibility verification, Petri nets, deadlock detection, structural analysis.

References:

• S.T. Albin, The art of software architecture: design methods and techniques; Wiley 2003.
• E.R. 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.266-271, 1994.
• A.W. Brown, "An overview of components and component-based development"; in Advances in Computers, vol.54 - Trends in Software Engineering, pp.1-34, Academic Press 2001.
• S. Chaki, E.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.388-402, 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.793-804, 1997.
• P. Clements, R. Kazman, M. Klein, Evaluating software architectures - methods and case studies; Addison-Wesley 2002.
• D.C. Craig, "Compatibility of software components - modeling and verification"; Ph.D. Thesis, Department of Computer Science, Memorial University, St.John's, Canada A1B 3X5, 2006.
• 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.11-18, 2006.
• J. Esparza, "Model checking using net unfolding"; Science of Computer Programming, vol.23, no.2-3, pp.151-195, 1994.
• D. Garlan, D.E. Perry, "Introduction to the special issue on software architecture"; IEEE Trans. on Software Engineering, vol.21, no.4, pp. 269-274, 1995.
• M. Hack, "Analysis of production schemata by Petri nets"; Technical Report TR-94, Massachusetts Institute of Technology, Cambridge, MA, USA, 1972.
• J.E. Hopcroft, R. Motwani, J.D. Ullman, Introduction to automata theory, languages, and computations (2 ed.); Addison Wesley 2001.
• R. Janicki, P.E. Lauer, Specification and analysis of concurrent systems - the COSY approach; Springer-Verlag 1992.
• T. Murata, "Petri nets: properties, analysis, and applications", Proceedings of the IEEE, vol.77, no.4, pp.541-580, 1989.
• W. Reisig, Petri nets - an introduction (EATCS Monographs on Theoretical Computer Science 4); Springer-Verlag 1985.
• M. Shaw, D. Garlan, Software architecture: perspectives on an emerging discipline; Prentice Hall 1996.
• M. Silva, E. Teruel, J. Couvreur, "Linear algebra in and linear programming techniques for the analysis of place/transition net systems"; in Lecture on Petri nets - basic models (Lecture Notes in Computer Science 1491), pp.309-373, Springer-Verlag 1998.
• C. Szyperski (with D. Gruntz, S. Murer), Component software: beyond object-oriented programming (2 ed.); Addison-Wesley 2002.
• S. Tanimoto, M. Yamaguchi, T. Watanabe, "Finding minimal siphons in general Petri nets", IEICE Trans. on Fundamentals in Electronics, Communications, and Computer Science vol.E79-A, no.11, pp.1817-1824, 1996.
• W.M Zuberek, "Timed Petri nets - definitions, properties and applications"; Microelectronics and Reliability (Special Issue on Petri Nets and Related Graph Models), vol.31, no.4, pp.627-644, 1991.

Available in pdf.