The General-Purpose Modeling, Analysis, and Implementation of Software Architectures

In this paper, a new software modeling language called SAMP is proposed, which is inspired from UML and enables the general-purpose modeling of software architectures but at the same time promotes the multiple-viewpoints modeling, formal verification of the models for the desired requirements, and combining model and code together. SAMP supports the high-level modeling of software architectures from the requirements, logical, behavioral, and deployment perspectives and supports checking the consistencies between the software models in different perspectives. SAMP is also supported with a modeling toolset that allows for the visual modeling of software architectures in those perspectives. The toolset further generates formal ProMeLa models that can be accepted by the SPIN model checker for the exhaustive verification of the software behaviors against the user-defined properties and some pre-defined properties (e.g., deadlock, race-condition, wrong and incomplete preconditions). Moreover, the toolset can also generate the Java Modeling Language (JML) code that combines the contractual models with the Java program for ensuring the consistency between model and code throughout the software development.

Yazılım Mimarilerinin Genel-amaçlı olarak Modellenmesi, Analizi, ve Koda Dönüştürülmesi

Bu makalede, endüstride sıklıkla kullanılan UML modelleme dilinden esinlenen SAMP adında yeni bir yazılım mimarisi modelleme dili önerilmektedir. SAMP ile, modellenen yazılım mimarileri, biçimsel yöntemler kullanılarak analiz edilebilir, ve sonrasında otomatik olarak koda dönüştürülebilir. SAMP, yazılım mimarilerinin gereksinim, mantıksal, davranışsal, ve fiziksel bakış açılarına göre ayrı ayrı modellenebilmesini desteklemektedir. Ayrıca, bir araç kümesi aracılığıyla, SAMP modelleri otomatik olarak ProMeLa biçimsel sınama dilinde modellere dönüştürülerek ProMeLa’yı destekleyen SPIN model sınayıcısıyla kapsamlı olarak analiz edilebilir ve kullanıcı-tanımlı ve önceden-tanımlı birçok özelliğin sağlanıp sağlanmadığı anlaşılabilir. Yine aynı araç desteği ile, analiz edilen modeller Java Modeling Language (JML) dilinde koda dönüştürülebilir. JML sayesinde, model ile Java kodunu bir arada yürütmek mümkün olup kodun modeli sağlayıp sağlamadığı JML’i destekleyen araçlar ile sürekli test edilebilir.

PDF

___

[1] J. E. Rumbaugh, I. Jacobson, and G. Booch, The unified modeling language reference manual, Addison- Wesley-Longman, 1999.

[2] M. Ozkaya, “Analysing uml-based software modelling languages,” Journal of Aeronautics and Space Technologies, vol 11, pp. 119-134, July 2018.

[3] M. Ozkaya, “The analysis of architectural languages for the needs of practitioners,” Softw., Pract. Exper., vol. 48, pp. 985-1018, January 2018.

[4] B. Meyer, J.-M. Nerson, and M. Matsuo, Objectoriented design for software engineering. Lecture Notes in Computer Science, vol. 289, pp. 221-229. Springer, 1987.

[5] G. T. Leavens, A. L. Baker, and C. Ruby, “Preliminary design of jml: A behavioral interface specification language for java,” SIGSOFT Softw. Eng. Notes, vol. 31, pp. 1-38, May 2006.

[6] G. J. Holzmann, The SPIN Model Checker - primer and reference manual, Addison-Wesley, 2004.

[7] R. Milner, J. Parrow, and D. Walker, “A calculus of mobile processes”, i. Inf. Comput., vol. 100, pp. 1-40, September 1992.

[8] C. A. R. Hoare, “Communicating sequential processes,” Commun. ACM, vol. 21, pp. 666-677, August 1978.

[9] A. van Deursen, P. Klint, and J. Visser, “Domainspecific languages: An annotated bibliography,” SIGPLAN Not., vol. 35, pp. 26-36, June 2000.

[10] L. T. W. Agner, I. W. Soares, P. C. Stadzisz, and J. M. SimaO, “A brazilian survey on uml and model-driven practices for embedded software development,” J. Syst. Softw., vol. 86, pp. 997-1005, April 2013.

[11] J. Hutchinson, J. Whittle, M. Rouncefield, and S. Kristoffersen, Empirical assessment of mde in industry. In Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, New York, NY, USA May 2011. pp. 471-480.

[12] P. Chalin, J. R. Kiniry, G. T. Leavens, and E. Poll, Beyond assertions: advanced specification and verification with jml and esc/java2. In Proceedings of the 4th international conference on Formal Methods for Components and Objects, FMCO’05, Berlin, Heidelberg, Springer-Verlag., November 2006. pp. 342-363.

[13] R. Behjati, T. Yue, L. Briand, and B. Selic, “Simpl: A product-line modeling methodology for families of integrated control systems,” Inf. Softw. Technol., vol. 55, pp. 607-629, March 2013.

[14] A. K. Andreas Kraus and N. Koch, Model-driven generation of web applications in uwe. In Proceedings of the 3rd International Workshop on Model-Driven Web Engineering, MDWE2007, pp. 23-38. CEUR-WS, 2007.

[15] P. H. Feiler, B. A. Lewis, and S. Vestal, The SAE architecture analysis & design language (AADL): A standard for engineering performance critical systems. In IEEE Intl Symp. on Intell. Control, pp. 1206-1211, October 2006

16] V. Debruyne, F. Simonot-Lion, and Y. Trinquet, “EAST-ADL | An Architecture Description Language”, pp. 181-195. Springer US, Boston, MA, 2005.

[17] J. H. McDuffie, Using the architecture description language metah for designing and prototyping an embedded reconfigurable sliding mode flight controller. In Proceedings of the 21st Digital Avionics Systems Conference, vol. 2, pp. 8B1-1-8B1-17, 2002.

[18] Y. Oh, D. H. Lee, S. Kang, and J. H. Lee, Extended architecture analysis description language for software product line approach in embedded systems. In Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE ’07, Washington, DC, USA, 2007. pp. 87-88.

[19] N. Ali, I. Ramos, and C. Solis, “Ambientprisma: Ambients in mobile aspect-oriented software architecture,” Journal of Systems and Software, vol. 83, pp. 937-958, October 2010.

[20] J. Perez, I. Ramos, J. J. Martinez, P. Letelier, and E. Navarro, Prisma: Towards quality, aspect oriented and dynamic software architectures. In QSIC, IEEE Computer Society, 2003. pp. 59-66

[21] L. Cardelli and A. D. Gordon, “Mobile ambients”, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 140- 155. 1998.

[22] D. Balasubramanian, A. Dubey, W. Otte, T. Levendovszky, A. Gokhale, P. Kumar, W. Emfinger, and G. Karsai, “DREMS ML: A wide spectrum architecture design language for distributed computing platforms,” Science of Computer Programming, vol. 106, pp. 3-29, August 2015.

[23] S. Becker, H. Koziolek, and R. Reussner, “The palladio component model for model-driven performance prediction,” Journal of Systems and Software, vol. 82, pp. 3-22, January 2009.

[24] P. Kruchten and C. J. Thompson, An object-oriented, distributed architecture for large-scale ada systems. In Proceedings of the Conference on TRI-Ada ’94, TRI-Ada ’94, New York, NY, USA, ACM. 1994. pp. 262-271

[25] J. Li, N. T. Pilkington, F. Xie, and Q. Liu, “Embedded architecture description language,” Journal of Systems and Software, vol. 83, pp. 235-252, February 2010.

[26] N. R. Mehta, N. Medvidovic, and S. Phadke, Towards a taxonomy of software connectors. In C. Ghezzi, M. Jazayeri, and A. L. Wolf, editors, ICSE, ACM, 2000. pp. 178-187

[27] B. Meyer, “Applying Design by Contract,” IEEE Computer, vol. 25, pp. 40-51, October 1992.

[28] E. Rodriguez, M. Dwyer, C. Flanagan, J. Hatcliff, G. T. Leavens, and Robby, Extending jml for modular specification and verify cation of multi-threaded programs. In Proceedings of the 19th European Conference on Object-Oriented Programming, ECOOP’05, Berlin, Heidelberg, Springer-Verlag. 2005. pp. 551-576,

[29] S. Kelly, K. Lyytinen, and M. Rossi, Metaedit+ A fully configurable multi-user and multi-tool CASE and CAME environment. In J. A. B. Jr., J. Krogstie, O. Pastor, B. Pernici, C. Rolland, and A. S lvberg, editors, Seminal Contributions to Information Systems Engineering, 25 Years of CAiSE, Springer 2013. pp. 109-129.

[30] G. Naumovich, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil, Applying static analysis to software architectures. In M. Jazayeri and H. Schauer, editors, ESEC / SIGSOFT FSE, volume 1301 of Lecture Notes in Computer Science, Springer, 1997. pp. 77-93.

[31] R. Allen and D. Garlan, A case study in architectural modelling: The aegis system. In Proceedings of the Eighth International Workshop on Software Specification and Design (IWSSD-8), Paderborn, Germany, March 1996. pp. 6-15.

[32] G. J. Holzmann, “An analysis of bitstate hashing,” Formal Methods in System Design, vol. 13, pp. 289-307, November 1998.

[33] B. Beckert, R. Hahnle, and P. H. Schmitt, Verification of Object-oriented Software: The KeY Approach, Springer-Verlag, Berlin, Heidelberg, 2007.

[34] D. R. Cok, Openjml: Jml for java 7 by extending openjdk. In M. Bobaru, K. Havelund, G. J. Holzmann, and R. Joshi, editors, NASA Formal Methods, Springer Berlin Heidelberg. 2011. pp. 472-479.