Abstract XCD is a design-by-contract based architecture description language that supports modular specifications in terms of components and connectors (i.e.,interaction protocols).XCD is supported by a translator that produces formal models in SPIN's ProMeLa formal verification language,which can then be formally analysed using SPIN's model checker. XCD is extended with a visual notation set called VXCD.VXCD extends UML's component diagram and adapts it to XCD's structure,contractual behaviour,and interaction protocol specifications.Visual VXCD specifications can be translated into textual XCD specifications for formal analysis.To illustrate VXCD,the well-known gas station system is used.The gas system is specified contractually using VXCD's visual notation set and then formally analysed using SPIN's model checker for a number of properties including deadlock and race-condition.
This work was supported by the Project of the Scientific and Technological Research Council of Turkey (TUBITAK) under Grant No. 215E159.
About author: Mert Ozkaya is assistant professor in Istanbul Kemerburgaz University, Istanbul. Dr. Ozkaya received his Ph.D. degree in computer science from City University London, London, in 2014. Previously, he received his M.S. degree in computer science from University of Essex, Colchester, in 2010, and his B.S. degree in computer engineering from Bilkent University, Ankara, in 2009.
Cite this article:
Mert Ozkaya.Visual Specification and Analysis of Contract-Based Software Architectures[J] Journal of Computer Science and Technology, 2017,V32(5): 1025-1043
 Clements P C, Garlan D, Little R, Nord R L, Stafford J A. Documenting software architectures:Views and beyond. In Proc. the 25th Int. Conf. Software Engineering, May 2003, pp.740-741. Bass L, Clements P, Kazman R. Software Architecture in Practice (3rd edition). Addison-Wesley Professional, 2012. Medvidovic N, Taylor R N. A classification and comparison framework for software architecture description languages. IEEE Trans. Software Engineering, 2000, 26(1):70-93. Rumbaugh J, Jacobson I, Booch G. The Unified Modeling Language Reference Manual (2nd edition). Pearson Higher Education, 2004. Ozkaya M, Kloukinas C. Are we there yet? Analyzing architecture description languages for formal analysis, usability, and realizability. In Proc. the 39th EUROMICRO Conf. Software Engineering and Advanced Applications, September 2013, pp.177-184. Lago P, Malavolta I, Muccini H, Pelliccione P, Tang A. The road ahead for architectural languages. IEEE Software, 2015, 32(1):98-105. Malavolta I, Lago P, Muccini H, Pelliccione P, Tang A. What industry needs from architectural languages:A survey. IEEE Trans. Software Engineering, 2013, 39(6):869-891. Ozkaya M, Kloukinas C. Design-by-contract for reusable components and realizable architectures. In Proc. the 17th Int. ACM SIGSOFT Symp. Component-Based Software Engineering, June 30-July 4, 2014, pp.129-138. Meyer B. Applying ‘design by contract’. Computer, 1992, 25(10):40-51. Cheon Y, Leavens G T. A simple and practical approach to unit testing:The JML and JUnit way. In Proc. the 16th European Conf. Object-Oriented Programming, June 2002, pp.231-255. Kiniry J R, Zimmerman D M. Secret ninja formal methods. In Proc. the 15th Int. Symp. Formal Methods, May 2008, pp.214-228. Holzmann G J. The SPIN Model Checker:Primer and Reference Manual. Addison-Wesley, 2004. Balmelli L. An overview of the systems modeling language for products and systems development. Journal of Object Technology, 2007, 6(6):149-177. Allen R, Garlan D. A formal basis for architectural connection. ACM Trans. Software Engineering and Methodology, 1997, 6(3):213-249. Magee J, Dulay N, Eisenbach S, Kramer J. Specifying distributed software architectures. In Proc. the 5th European Software Engineering Conf., September 1995, pp.137-153. van Ommering R C, van der Linden F, Kramer J, Magee J. The koala component model for consumer electronics software. Computer, 2000, 33(3):78-85. Feiler P H, Gluch D P, Hudak J J. The architecture analysis & design language (AADL):An introduction. Technical Note CMU/SEI-2006-TN-011, Carnegie Mellon University, 2006. Hoare C A R. Communicating sequential processes. Communications of the ACM, 1978, 21(8):666-677. Milner R, Parrow J, Walker D. A calculus of mobile processes, I. Information and Computation, 1992, 100(1):1-40. Banach R. Review:Handbook of process algebra. Journal of Logic and Computation, 2003, 13(6):959-962. Murata T. Petri nets:Properties, analysis and applications. Proc. the IEEE, 1989, 77(4):541-580. Völzer H. An overview of BPMN 20 and its potential use. In Proc. the 2nd Int. Workshop on Business Process Modeling Notation, October 2010, pp.14-15. Ali N, Ramos I, Solís C. Ambient-PRISMA:Ambients in mobile aspect-oriented software architecture. Journal of Systems and Software, 2010, 83(6):937-958. Faucou S, Déplanche A M, Trinquet Y. An ADL centric approach for the formal design of real-time systems. In Proc. World Computer Congress IFIP TC-2 Workshop on Architecture Description Languages, August 2004, pp.67-82. Poizat P, Royer J C. KORRIGAN:A formal ADL with full data types and a temporal glue. Technical Report N°88-2003, Laboratoire de Methodes Informatiques, 2003. Oquendo F. πADL:An architecture description language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT Software Engineering Notes, 2004, 29(3):1-14. Yu Z H, Cai Y L, Wang R F, Han J Q. π-net ADL:An architecture description language for multi-agent systems. In Proc. the Int. Conf. Advances in Intelligent Computing, August 2005, pp.218-227. Pérez J, Ali N, Carsí J A, Ramos I. Designing software architectures with an aspect-oriented architecture description language. In Proc. the 9th Int. Conf. Component-Based Software Engineering, June 29-July 1, 2006, pp.123-138. Bjørk J, Hagalisletto A M. Challenges in simulating railway systems using Petri Nets. Technical Report, Department of Informatics, University of Oslo, 2005. Liu F, Heiner M. Colored petri nets to model and simulate biological systems. In CEUR Workshop Proc., Donatelli S, Kleijn J, Machado R J, Fernandes J M (eds.), June 2012, pp.71-85. Chatain T, Fabre E. Factorization properties of symbolic unfoldings of colored Petri Nets. In Proc. the 31st Int. Conf. Applications and Theory of Petri Nets, June 2010, pp.165-184. Taylor R N, Medvidovic N, Dashofy E M. Software Architecture:Foundations, Theory, and Practice. Wiley, 2009. Rademaker A, Braga C, Sztajnberg A. A rewriting semantics for a software architecture description language. Electronic Notes in Theoretical Computer Science, 2005, 130:345-377. Reussner R H, Schmidt H W, Poernomo I H. Reliability prediction for component-based software architectures. Journal of Systems and Software, 2003, 66(3):241-252. Lau K, Tran C M. X-MAN:An MDE tool for componentbased system development. In Proc. the 38th EUROMICRO Conf. Software Engineering and Advanced Applications, September 2012, pp.158-165. Kelly S, Lyytinen K, Rossi M. MetaEdit+ A fully configurable multi-user and multitool CASE and CAME environment. In Seminal Contributions to Information Systems Engineering, Bubenko J, Krogstie J, Pastor O, Pernici B, Rolland C, Sølvberg A (eds.), Springer, 2013, pp.109-129. Naumovich G, Avrunin G S, Clarke L A, Osterweil L J. Applying static analysis to software architectures. In Proc. the 6th European SOFTWARE ENGINEERING Conf. Held Jointly with the 5th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, September 1997, pp.77-93. Holzmann G J. An analysis of bitstate hashing. Formal Methods in System Design, 1998, 13(3):289-307. Aldrich J, Chambers C, Notkin D. ArchJava:Connecting software architecture to implementation. In Proc. the 24th Int. Conf. Software Engineering, May 2002, pp.187-197.
Copyright 2010 by Journal of Computer Science and Technology