Event strictness for components with complex bindings

ABSTRACT

Component Based Software Engineering has been investigated to improve software modularity. Various component models exist, but improvements are still needed to provide architecture validation. In this paper, we present a hierarchical component model using explicit protocols defined with the Symbolic Transition System (STS) formalism. This model is based on an N-party rendezvous and provides three new kinds of bindings. We formalise our model and define two orthogonal properties: behavioural compatibility and event strictness. We also present preliminary results about the check of these properties.

REFERENCES

• 1: The Fractal Composition Framework, June 2002. www.objectweb.org.
• 2: Jonathan Aldrich , Craig Chambers , David Notkin, ArchJava: connecting software architecture to implementation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581365]
• 3: R. Allen, R. Douence, and D. Garlan. Specifying and Analyzing Dynamic Software Architectures. In FASE'98, volume 1382 of Lecture Notes in Computer Science, pages 21--37. Springer-Verlag, 1998.
• 4: Robert Allen , David Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.3, p.213-249, July 1997 [doi>10.1145/258077.258078]
• 5: AMPLE. Aspect-oriented, model-driven product line engineering. www.project-ample.net, 2008.
• 6: P. André, G. Ardourel, and C. Attiogbé. Defining Component Protocols with Service Composition: Illustration with the Kmelia Model. In M. Lumpe and
• 7: W. Vanderperren, editors, Software Composition, volume 4829 of LNCS, pages 2--17. Springer, 2007.
• 8: André Arnold , John Plaice, Finite transition systems: semantics of communicating systems, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 9: André Arnold , Gérald Point , Alain Griffault , Antoine Rauzy, The AltaRica formalism for describing concurrent systems, Fundamenta Informaticae, v.40 n.2-3, p.109-124, Nov. 1999
• 10: Egidio Astesiano , Hans-Joerg Kreowski , Bernd Krieg-Brueckner, Algebraic Foundations of Systems Specification, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 11: Tomás Barros , Antonio Cansado , Eric Madelaine , Marcela Rivera, Model-checking Distributed Components: The Vercors Platform, Electronic Notes in Theoretical Computer Science (ENTCS), 182, p.3-16, June, 2007 [doi>10.1016/j.entcs.2006.09.028]
• 12: T. Barros, L. Henrio, and E. Madelaine. Behavioural Models for Hierarchical Components. In Proc. of SPIN'05, volume 3639 of LNCS, pages 154--168. Springer-Verlag, 2005.
• 13: H. Baumeister, F. Hacklinger, R. Hennicker, A. Knapp, and M. Wirsing. A Component Model for Architectural Programming. In Proc. 2nd Int. Wsh. Formal Aspects of Component Software (FACS'05), volume 160 of ENTCS, pages 75--96, 2005.
• 14: Andrea Bracciali , Antonio Brogi , Carlos Canal, A formal approach to component adaptation, Journal of Systems and Software, v.74 n.1, p.45-54, January 2005 [doi>10.1016/j.jss.2003.05.007]
• 15: Luboš Brim , Ivana Černá , Pavlína Vařeková , Barbora Zimmerova, Component-interaction automata as a verification-oriented component-based system specification, Proceedings of the 2005 conference on Specification and verification of component-based systems, September 05-06, 2005, Lisbon, Portugal
• 16: Tomas Bures , Petr Hnetynka , Frantisek Plasil, SOFA 2.0: Balancing Advanced Features in a Hierarchical Component Model, Proceedings of the Fourth International Conference on Software Engineering Research, Management and Applications, p.40-48, August 09-11, 2006 [doi>10.1109/SERA.2006.62]
• 17: M. Calder, S. Maharaj, and C. Shankland. A Modal Logic for Full LOTOS Based on Symbolic Transition Systems. The Computer Journal, 45(1):55--61, 2002.
• 18: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 19: F. Fernandes and J.-C. Royer. The STSLIB Project: Towards a Formal Component Model Based on STS. Formal Aspect of Component Software Workshop, 2007.
• 20: G. Gößler, S. Graf, M. Majster-Cederbaum, M. Martens, and J. Sifakis. An approach to modeling and verification of component based systems. volume 4362, pages 61--70, 2007.
• 21: Susanne Graf , Sophie Quinton, Contracts for BIP: Hierarchical Interaction Models for Compositional Verification, Proceedings of the 27th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems, June 27-29, 2007, Tallinn, Estonia [doi>10.1007/978-3-540-73196-2_1]
• 22: Serge Haddad , Pascal Poizat, Transactional Reduction of Component Compositions, Proceedings of the 27th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems, June 27-29, 2007, Tallinn, Estonia [doi>10.1007/978-3-540-73196-2_22]
• 23: A. Ingolfsdottir and H. Lin. A Symbolic Approach to Value-passing Processes, chapter Handbook of Process Algebra. Elsevier, 2001.
• 24: B. Jeannet, T. Jéron, V. Rusu, and E. Zinovieva. Symbolic Test Selection Based on Approximate Analysis. In TACAS'2005, volume 3440 of LNCS, pages 349--364. Springer-Verlag, 2005.
• 25: J. Kramer, J. Magee, and S. Uchitel. Software Architecture Modeling and Analysis: A Rigorous Approach. In Proc. of SFM'03, volume 2804 of LNCS, pages 44--51. Springer-Verlag, 2003.
• 26: Nenad Medvidovic , Richard N. Taylor, A Classification and Comparison Framework for Software Architecture Description Languages, IEEE Transactions on Software Engineering, v.26 n.1, p.70-93, January 2000 [doi>10.1109/32.825767]
• 27: R. Milner. Calculi for synchrony and asynchrony. TCS: Theoretical Computer Science, 25:267--310, 1983.
• 28: Frantisek Plasil , Stanislav Visnovsky, Behavior Protocols for Software Components, IEEE Transactions on Software Engineering, v.28 n.11, p.1056-1076, November 2002 [doi>10.1109/TSE.2002.1049404]
• 29: P. Poizat and J.-C. Royer. A Formal Architectural Description Language based on Symbolic Transition Systems and Modal Logic. Journal of Universal Computer Science, 12(12):1741--1782, 2006.
• 30: P. Poizat, J.-C. Royer, and G. Salaün. Bounded Analysis and Decomposition for Behavioural Description of Components. In Springer Verlag, editor, FMOODS, number 4037 in LNCS, pages 33--47, 2006.
• 31: J.-C. Royer. The STSLib project. www.emn.fr/x-info/~jroyer/WEBLIB, 2008.
• 32: Daniel M. Yellin , Robert E. Strom, Protocol specifications and component adaptors, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.292-333, March 1997 [doi>10.1145/244795.244801]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Languages (e.g., description, interconnection, definition)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Validation

General Terms:
Languages, Verification

Keywords:
behavioural compatibility, binding, communication, component, event strictness, protocol, structured product