Trustworthy Assembly of Components using the B Refnement

• Autorzy: Lanoix A. , Souquiferes J.
• Języki publikacji: EN

Abstrakty

EN

In component-based software development approaches, omponents are considered as black boxes, communicating through required and provided interfaces which describe their visible behaviors. In the best cases, the provided interfaces are checked to be compatible with the corresponding required interfaces, but in general, adapters have to be introduced to connect them. We propose to exploit existing notations and languages with their associated tools to specify working systems out of components: UML composite structure diagrams to express the architecture in terms of components and their interfaces, class diagrams, sequence diagrams and protocol state machines to describe the behavior of each component. Component interfaces will then be expressed in B in order to verify the interoperability. The use of B assembling and refnement mechanisms eases the verifcation of the interoperability between interfaces and the correctness of the component assembly.

Słowa kluczowe

EN

refnement mechanizm; based software; Simple Access Control System

• Wydawca: Oficyna Wydawnicza Politechniki Wrocławskiej
• Czasopismo: e-Informatica Software Engineering Journal
• Rocznik: 2008
• Tom: Vol. 2, nr 1
• Strony: 9--23
• Opis fizyczny: Bibliogr. 36 poz.

Twórcy

autor

Lanoix A.

autor

Souquiferes J.

• LORIA Nancy-Universitfe, CNRS

Bibliografia

• [1] J.-R. Abrial. The B Book. Cambridge University Press, 1996.
• [2] AFADL'2000. Etude de cas : systfeme de contr^ole d'accfes. In Journfees AFADL, Approches formelles dans l'assistance au dfeveloppement de logiciels, 2000. actes LSR/IMAG.
• [3] L. Alfaro and T. A. Henzinger. Interface automata. In 9th Annual Aymposium on Foundations of Software Engineering, FSE, pages 109{120. ACM Press, 2001.
• [4] P. Behm, P. Benoit, and J. Meynadier. METEOR: A Successful Application of B in a Large Project. In Integrated Formal Methods, IFM99, volume 1708 of LNCS, pages 369{387. Springer Verlag, 1999.
• [5] D. Bert, S. Boulmfe, M.-L. Potet, A. Requet, and L. Voisin. Adaptable Translator of B Specifcations to Embedded C Programs. In Integrated Formal Method, IFM'03, volume 2805 of LNCS, pages 94{113. Springer Verlag, 2003.
• [6] D. Beyer, A. Chakrabarti, and T. A. Henzinger. Web service interfaces. In Proceedings of the 14th International World Wide Web Conference (WWW 2005), pages 148{159. ACM Press,2005.
• [7] A. Bracciali, A. Brogi, and C. Canal. A formal approach to component adaptation. In Journal of Systems and Software, volume 74, pages 45{54. Elsevier Science Inc., 2005.
• [8] A. W. Brown and K. C. Wallnan. Engineering of component-based systems. In Proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer Systems (ICECCS '96), page 414. IEEE Computer Society, 1996.
• [9] C. Canal, L. Fuentes, E. Pimentel, J.-M. Troya, and A. Vallecillo. Extending CORBA interfaces with protocols. Computer Journal, 44(5):448{462, 2001.26 Arnaud Lanoix, Jeanine Souquiferes
• [10] C. Canal, J. M. Murillo, and P. Poizat. Software adaptation. L'Objet, 12(1):9{31, 2006.
• [11] S. Chouali, M. Heisel, and J. Souquiferes. Proving Component Interoperability with B Refnement. Electronic Notes in Theoretical Computer Science (ENTCS), 160:157{172, 2006.
• [12] S. Chouali and J. Souquiferes. Verifying the compatibility of component interfaces using the B formal method. In International Conference on Software Engineering Research and Practice (SERP'05), pages 850{856. CSREA Press, 2005.
• [13] Clearsy. B4free, 2004. http://www.b4free.com.
• [14] I. Crnkovic, S. Larsson, and M. Chaudron. Component-based development process and component lifecycle. In 27th International Conference Information Technology Interfaces (ITI).IEEE, 2005.
• [15] E. Estevez and P. Fillottrani. Algebraic Specifcations and Refnement for Component-Based Development using RAISE. Journal of Computer Science and Technologie, 2(7):28{33, 2002.
• [16] D. Garlan, R. Allen, and J. Ockerbloom. Architectural Mismatch: Why Reuse is so Hard.IEEE Software, 12(6):17{26, 1999.
• [17] J. Han. A comprehensive interface defnition framework for software components. In The 1998 Asia Pacifc software engineering conference, pages 110{117. IEEE Computer Society,1998.
• [18] J. Han. Temporal logic based specifcation of component interaction protocols. In Proceedings of the Second Workshop on Object Interoperability ECOOP'2000, pages 12{16. Springer Verlag, 2000.
• [19] D. Hatebur, M. Heisel, and J. Souquiferes. A Method for Component-Based Software and System Development. In Proceedings of the 32nd Euromicro Conference on Software Engineering And Advanced Applications, pages 72{80. IEEE Computer Society, 2006.
• [20] G. Heineman and H. Ohlenbusch. An evaluation of component adaptation techniques. Technical Report WPI-CS-TR-98-20, Department of Computer Science, Worcester Polytechnic Institute, February 1999.
• [21] M. Heisel, T. Santen, and J. Souquiferes. Toward a formal model of software components. In Proc. 4th International Conference on Formal Engineering Methods - ICFEM'02, number 2495 in LNCS, pages 57{68. Springer-Verlag, 2002.
• [22] H. Ledang and J. Souquiferes. Modeling class operations in B: application to UML behavioral diagrams. In ASE'2001 : 16th IEEE International Conference on Automated Software Engineering, pages 289{296. IEEE Computer Society, 2001.
• [23] H. Ledang and J. Souquiferes. Contributions for modelling UML state-charts in B. In Third International Conference on Integrated Formal Methods - IFM'2002, pages 109{127, Turku,Finland, 2002.
• [24] E. Meyer and J. Souquiferes. A systematic approach to transform OMT diagrams to a B specifcation. In Proceedings of the Formal Method Conference, number 1708 in LNCS, pages 875{895. Springer-Verlag, 1999.
• [25] Microsoft. .Net. http://www.microsoft.com/net.
• [26] I. Mouakher, A. Lanoix, and J. Souquiferes. Component Adaptation: Specifcation and Verifcation. In Proc. of the 11th Int. Workshop on Component Oriented Programming (WCOP'06),satellite workshop of ECOOP 2006, pages 23{30, 2006.Trustworthy Assembly of Components using the B Refnement 27
• [27] Object Management Group (OMG). UML Superstructure Specifcation, 2005. version 2.0.
• [28] Object Mangagement Group (OMG). Corba Component Model Specifcation, 2006. version 4.0.
• [29] R. H. Reussner, H. W. Schmidt, and I. H. Poernomo. Reasoning on software architectures with contractually specifed components. In A. Cechich, M. Piattini, and A. Vallecillo, editors, Component-Based Software Quality: Methods and Techniques, pages 287{325. 2003.
• [30] H. W. Schmidt and R. H. Reussner. Generating adapters fo concurrent component protocol synchronisation. In I. Crnkovic, S. Larsson, and J. Staford, editors, Proceeding of the 5th IFIP International conference on Formal Methods for Open Object-based Distributed Systems,pages 213{229, 2002.
• [31] Steria { Technologies de l'information. Obligations de preuve: Manuel de rfefference, version 3.0, 1998.
• [32] Sun Microsystems. JSR 220: Enterprise JavaBeans, 2006. Version 3.0, Final Realase.
• [33] C. Szyperski. Component Software. ACM Press, Addison-Wesley, 1999.
• [34] W3C. Web Services. http://www.w3.org/2002/ws.
• [35] D. D. M. Yellin and R. E. Strom. Protocol specifcations and component adaptors. ACM Transactions on Programming Languages and Systems, 19(2):292{333, 1997.
• [36] A. M. Zaremski and J. M. Wing. Specifcation matching of software components. ACM Transaction on Software Engeniering Methodolology, 6(4):333{369, 1997.