Login Register Cart 0
Generic placeholder image

Recent Advances in Computer Science and Communications

Editor-in-Chief

ISSN (Print): 2666-2558
ISSN (Online): 2666-2566

Back
Journal Home About Journal Editorial Board Current Issue Volumes/Issues
Subscribe
General Research Article

A Comparative Study on Transformation of UML/OCL to Other Specifications

Author(s): Jagadeeswaran Thangaraj* and Senthilkumaran Ulaganathan

Volume 13, Issue 2, 2020

Page: [256 - 264] Pages: 9

DOI: 10.2174/2213275912666190129121059

Price: $65

Abstract

Background: Static verification is a sound programming methodology that permits automated reasoning about the correctness of an implementation with respect to its formal specification before its execution. Unified Modelling Language is most commonly used modelling language which describes the client’s requirement. Object Constraint Language is a formal language which allows users to express textual constraints regarding the UML model. Therefore, UML/OCL express formal specification and helps the developers to implement the code according to the client’s requirement through software design.

Objective: This paper aims to compare the existing approaches generating Java, C++, C# code or JML, Spec# specifications from UML/OCL.

Method: Nowadays, software system is developed via automatic code generation from software design to implementation when using formal specification and static analysis. In this paper, the study considers transformation from design to implementation and vice versa using model transformation, code generation or other techniques.

Results: The related tools, which generate codes, do not support verification at the implementation phase. On the other hand, the specification generation tools do not generate all the required properties which are needed for verification at the implementation phase.

Conclusion: If the generated system supports the verification with all required properties, code developer needs less efforts to produce correct software system. Therefore, this study recommends introducing a new framework which can act as an interface between design and implementation to generate verified software systems.

Keywords: Model transformation, UML, OCL, Spec#, JML, formal specifications, static verification.

Graphical Abstract

[1]
V. Rastogi, "Software development life cycle models - comparison, consequences", Int. J. Comp. Sci. Info. Tech., vol. 6, no. 1, pp. 168-172, 2015.
[2]
P. Barthelmess, and K.M. Anderson, A view of software development environments based on activity theory.Computer Supported Cooperative Work., Kluwer Academic Publishers: New York, 2002, pp. 1-2.
[3]
T. Gary, Leavens, Yoonsik Cheon: Design by contract with JML, ACM. Available from:, http://www.eecs.ucf.edu/leavens/JML/jmldbc.pdf
[4]
M. Huisman, W. Ahrendt, D. Bruns, and M. Hentschel, Formal specification with JML.. : Karlsruhe: Department of Informatics,Karlsruhe Institute of Technology, , 2014
[5]
H. Amjad, Combining model checking and theorem proving..Cambridge:Computer Laboratory, Department of Computer Science,University of Cambridge, 2004
[6]
P. Müller, "Reasoning about Object Structures Using Ownership, Verified Software: Theories, Tools, Experiments", In: Working Conference on Verified Software: Theories, Tools, and Experiments.Springer, Berlin, Heidelberg, 2005, pp. 93-104
[7]
T. Wrigstad, Ownership-Based Alias Management. Stockholm., Computer and Systems Sciences, KTH Information and Communication Technology: Sweden, 2006.
[8]
A. Mycroft, and J. Voigt, "Notions of aliasing and ownership, aliasing in object-oriented programming", In: Aliasing in Object-Oriented Programming. Types, Analysis and Verification., Springer: Berlin, Heidelberg, 2013, pp. 59-83.
[9]
J. Hogg, D. Lea, A. Wills, D. de Champeaux, and R. Holt, "The geneva convention on the treatment of object aliasing, aliasing in object- oriented programming", In: Aliasing in Object-Oriented Programming. Types, Analysis and Verification., Springer: Berlin, Heidelberg, 2013, pp. 7-14.
[10]
D. Clarke, J. Astlund, and T. Wrigstad, "Ownership types: A survey, aliasing in object oriented programming", In: Aliasing in Object-Oriented Programming. Types, Analysis and Verification., Springer: Berlin, Heidelberg, 2013, pp. 15-58.
[11]
W. Dietl, and P. Müller, "Object ownership in program verification, aliasing in object-oriented programming", In: Aliasing in Object-Oriented Programming. Types, Analysis and Verification., Springer: Berlin, Heidelberg, 2013, pp. 289-318.
[12]
A. Schaad, "Inferring universe annotations on the presence of ownership transfer, software component technology group” Zurich: Diss. Master’s thesis, Department of computerscience,ETH,2007. Available from:", http://sct. ethz. ch/projects/student_docs/Annetta_ Schaad, 2007
[13]
H. Shimba, K. Hanada, K. Okano, and S. Kusumoto, "Bidirectional translation between OCL and JML for round-trip engineering", 20th Asia-Pacific Software Engineering Conference (APSEC). Bangkok, 2013, pp. 49-54
[http://dx.doi.org/10.1109/APSEC.2013.111]
[14]
B. Perez, and I. Porres, "An overall framework for reasoning about UML/OCL models based on constraint logic programming and MDA", Int. J. Advan. Software: ICSEA, vol. 7, no. 1, pp. 370-380, 2013.
[15]
"OMG", Unified Modeling Language (UML): Version 2.4.1. Object Management Group.Available from:, http://www.omg.org/spec/UML/2.4.1
[16]
"OMG", Object Constraint Language(OCL): Version 2.3.1. Object Management Group.Available from:, http://www.omg.org/spec/OCL/2.3.1
[17]
J. Cabot, and M. Gogolla, "Object Constraint Language (OCL): A definitive guide", In: International School on Formal Methods for the Design of Computer, Communication and Software Systems., Springer: Berlin, Heidelberg, 2012, pp. 58-90.
[18]
M. Barnett, K.R. Leino, and W. Schulte, "The Spec# programming system: An overview", In: Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS)., Springer: Berlin, Heidelberg, 2004, pp. 46-69.
[19]
K.R.M. Leino, "P. Müller, Using the Spec# language, methodology, and tools to write bug-free programs", In: Advanced Lectures on Software Engineering., Springer: Berlin, Heidelberg, 2007, pp. 91-139.
[20]
M. Barnett, "R. Leino, W. Schulte and P. Muller, “Specification and Verification: The Spec# Experience", Commun. ACM. Vol.54, No.6,2011, pp. 81-91
[21]
K.R.M. Leino, and P. Müller, "Object Invariants in Dynamic Contexts", European Conference on Object-Oriented Programming.Springer, Berlin, Heidelberg, 2004, pp.491-515
[22]
P. Müller, " Modular Specification and Verification of Object Oriented programs, PhD thesis, Springer-Verlag, Fern Universitat Hagen, Germany,", 2002
[23]
W. Dietl, and P. Müller, "Universes: Lightweight ownership for JML", J. Object Technol., vol. 4, no. 8, pp. 5-32, 2005.
[24]
D. Cunningham, W. Dietl, S. Drossopoulouand, A. Francalanza, P. Muller, and A.J. Summers, "Universe types for topology and encapsulation", J. Form. Meth. Compon. Obj.,Springer-Verlag, . 2008, pp.72-112.
[http://dx.doi.org/10.1007/978-3-540-92188-2_4]
[25]
C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata, "Extended static checking for Java", Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation. 2002, pp. 234-245
[26]
W. Ahrendt, B. Beckert, R. Hahnle, M. Hentschel, R. Bubel, and P.H. Schmitt, "Formal verification with key, deductive software verification - The KeY book: From theory to practice", Springer, LNCS, vol. 10001, pp. 541-570, 2016.
[27]
F. Heidenreich, C. Wende, and B. Demuth, A framework for generating query language code from OCL invariants.Electronic Communications of the EASST, . Vol. 9, 2007
[28]
"INRIA", ATL transformation example: UML 2 Java, eclipse frame-work.Available from:, http://www.eclipse.org/atl/ atlTransformations/ UML2Java/
[29]
L. Siwik, K. Lewandowski, A. Wos, R. Drezewski, and M. Kisiel-Dorohinicki, UML2SQL: A tool for model-driven development of data access Layer.Smart Information and Knowledge Management., Springer: Berlin, Heidelberg, 2010, pp. 227-246.
[30]
K. Lano, S. Kolahdouz-Rahimi, S. Yassipour-Tehrani, and M. Sharbaf, "A survey of model transformation design pattern usage", In: International Conference on Theory and Practice of Model Transformations. Springer, Cham, 2017, pp. 108-118
[http://dx.doi.org/10.1007/978-3-319-61473-1_8]
[31]
A. Hamie, "Using patterns to map OCL constraints to JML Specifications", In: International Conference on Model-Driven Engineering and Software Development. Springer, Cham, 2015, pp. 35-48
[32]
A. Hamie, "Pattern-based mapping of OCL specifications to JML contracts", 2014 2nd International Conference on Model-Driven Engineering and Software Development (MODELS-WARD)", Lisbon, IEEE,. 193-200, 2015
[33]
K. Hanada, H. Shimba, K. Okano, and S. Kusumoto, "Implementation of a prototype bi-directional translation tool between OCL and JML", J. Informatics Society, vol. 5, no. 2, pp. 89-95, 2013.
[34]
J. Thangaraj, "Adding ownership constraints to OCL to automatically generate Spec# skeletons", Department of Computer Science, Master’s Thesis, Maynooth University. Ireland, 2015
[35]
T. Vajk, and G. Mezei, "Incremental OCL to C# code generation", In: IEEE Interna-tional Joint Conferences on Computational Cybernetics and Technical Informatics (ICCC-CONTI 2010)., IEEE, 2010, pp. 277-280.
[36]
R. Moiseev, S. Hayashi, and M. Saeki, "Generating assertion code from OCL: A transformational approach based on similarities of implementation languages", In: International Conference on Model Driven Engineering Languages and Systems.Springer, Berlin, Heidelberg, 2009, pp. 650-664
[37]
K. Lano, Agile Model-based Development using UML-RSDS., CRC Press: Boca Raton, Florida, United States, 2017.
[http://dx.doi.org/10.1201/9781315368153]
[38]
K. Lano, "Families to Persons Case with UML-RSDS", In: Proceedings of the 10th Transformation Tool Contest, a part of the Software Technologies: Applications and Foundations (STAF 2017) federation of conferences. Ed. by Antonio Garcia-Dominguez, Georg Hinkel, and Filip Krikava. CEUR Workshop Proceedings..Marburg, Germany CEUR-WS. org., 2017
[39]
K. Lano, The UML-RSDS Manual, 2018.Available from:, https://nms.kcl.ac.uk/ kevin.lano/uml2web/uml rsds.pdf
[40]
G. Ramesh, "XRTSDIC: Model Transformation from PIM to PSM", Intl. J. Engin.Tech.(UAE), vol. 7, no. 18, pp. 92-98, 2018.
[41]
P. Niemann, N. Przigoda, R. Wille, and R. Drechsler, "Analyzing frame conditions in uml/ocl models - consistency equivalence and independence", 6th International Conference on Model-Driven Engineering and Software Development. 2018, pp. 139-151
[http://dx.doi.org/10.5220/0006602301390151]

Rights & Permissions Print Cite
Article Metrics
2
© 2024 Bentham Science Publishers | Privacy Policy