Article

Automated size analysis for OCL

Authors:

ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

Pages 331 - 340

https://doi.org/10.1145/1287624.1287671

Published: 07 September 2007 Publication History

Get Access

Abstract

An essential tool in object oriented modeling is the specification of cardinalities of associations between classes. In Object Constraint Language (OCL) such constraints are expressed as conditions on the sizes of the collections that correspond to associations. In this paper we present tools and techniques for automated verification of size properties of collection types in OCL. We automatically verify invariants related to the sizes of the collections of a class with respect to the pre and post-conditions of the methods of that class. Our approach is based on a size abstraction that abstracts away the contents of the collections, but preserves the constraints on their sizes. We implemented a tool which automates this abstraction by converting OCL expressions on collections to arithmetic expressions on their sizes. Following this translation, we employ an infinite state model checker, called Action Language Verifier (ALV), for size analysis. Size abstraction reduces the state space of the system and, hence, the cost of automated verification, and by focusing on size properties, enables us to use efficient, domain specific model checking techniques for automated verification. To demonstrate the effectiveness of our approach we conducted a case study on the OCL specification of the Java Card API. The OCL specification of the Java Card API consists of 31 classes and 150 methods. Using our tool, we translated the OCL specification of each class to Action Language and verified the size properties using ALV. Verification with ALV took only a few seconds per class and we revealed errors in 26 out of the 150 method specifications.

References

[1]

Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hahnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. "The KeY Tool." Software and Systems Modeling vol. 4, no. 1, pp. 32--54, 2005.

Digital Library

Google Scholar

[2]

Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen. "Verifying Safety Policies with Size Properties and Alias Controls." In Proc. ICSE '05 St. Louis, MO, USA, pp. 186--195, 2005.

Digital Library

Google Scholar

[3]

Andy Evans, Robert B. France, Ana M. D. Moreira, Bernhard Rumpe. "Using Alloy and UML/OCL to Specify Run-Time Configuration Management:A Case Study." In Practical UML-Based Rigorous Development Methods UML01 Oct 2001, Toronto, Canada.

Digital Library

Google Scholar

[4]

Jonathan Edwards, Daniel Jackson, Technology Emina Torlak. "A Type System for Object Models." In Proc. of FSE '04 Newport Beach, CA, pp. 189--199, 2004.

Digital Library

Google Scholar

[5]

Martin Gogolla, Jorn Bohling, and Mark Richters. "Validation of UML and OCL Models by Automatic Snapshot Generation." In Proc. UML 2003 Springer, Berlin, LNCS 2863, 2003.

Google Scholar

[6]

John Hughes, Lars Pareto, Amr Sabry. "Proving the Correctness of Reactive Systems Using Sized Types." In Proc. POPL '96 pp. 410--423, 1996.

Digital Library

Google Scholar

[7]

Daniel Jackson. "Alloy:A Lightweight Object Modelling Notation." ACM Transactions on Software Engineering and Methodology vol. 11, no. 2, pp. 256--290, 2002.

Digital Library

Google Scholar

[8]

Viktor Kuncak and Daniel Jackson. "Relational Analysis of Algebraic Datatypes." In Proc. ESEC/FSE 2005 Lisbon, Portugal, September 5-9, 2005.

Digital Library

Google Scholar

[9]

Daniel Larsson and Wojciech Mostowski. "Specifying Java Card API in OCL." OCL 2. 0 Workshop at UML 2003, San Francisco, Electronic Notes in Theoretical Computer Science vol. 102 pp. 3-19, 2004,

Digital Library

Google Scholar

[10]

OMG. "Object Constraint Language Specification." In OMG Unified Modeling Language Specification, Version 1. 3, June 1999.

Google Scholar

[11]

OMG. "OMG Unified Modeling Language Specification, Version 1.3." Object Management Group, Inc., Framingham, Mass., Internet:http://www.omg.org, 1999.

Google Scholar

[12]

Mark Richters and Martin Gogolla. "Validating UML models and OCL constraints." In Proc. UML 2000 Springer, York, UK, LNCS 1939, 2000.

Digital Library

Google Scholar

[13]

Jos Warmer and Anneke Kleppe. "The Object Constraint Language: Precise Modeling with UML." Addison-Wesley, 1998.

Digital Library

Google Scholar

[14]

Tuba Yavuz-Kahveci, Constantinos Bartzis, and Tevfik Bultan. "Action Language Verifier, Extended." In Proc. CAV'05 LNCS 3576, pp. 413--427, 2005.

Digital Library

Google Scholar

Cited By

View all

Marussy KSemerath OVarro D(2022)Automated Generation of Consistent Graph Models With Multiplicity ReasoningIEEE Transactions on Software Engineering10.1109/TSE.2020.302573248:5(1610-1629)Online publication date: 1-May-2022
https://doi.org/10.1109/TSE.2020.3025732
Clariso RGonzalez CCabot J(2019)Smart Bound Selection for the Verification of UML/OCL Class DiagramsIEEE Transactions on Software Engineering10.1109/TSE.2017.277783045:4(412-426)Online publication date: 1-Apr-2019
https://doi.org/10.1109/TSE.2017.2777830
Chavez HShen WFrance RMechling BLi G(2016)An Approach to Checking Consistency between UML Class Model and Its Java ImplementationIEEE Transactions on Software Engineering10.1109/TSE.2015.248864542:4(322-344)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1109/TSE.2015.2488645
Show More Cited By

Index Terms

Automated size analysis for OCL
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Classes and objects
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

Verification-driven slicing of UML/OCL models
ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

Model defects are a significant concern in the Model-Driven Development (MDD) paradigm, as model transformations and code generation may propagate errors to other notations where they are harder to detect and trace. Formal verification techniques can ...
Transformation of TOCL temporal properties into OCL
MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings

Specifying and verifying the temporal properties of UML-based systems can be challenging. Although there exist some extensions of OCL to support the specification of temporal properties, most of the approaches depend on using non-UML formalisms such as ...
HOL-OCL: a formal proof environment for UML/OCL
FASE'08/ETAPS'08: Proceedings of the Theory and practice of software, 11th international conference on Fundamental approaches to software engineering

We present the theorem proving environment HOLOCL that is integrated in a Model-driven Engineering (MDE) framework. HOLOCL allows to reason over uml class models annotated with OCL specifications. Thus, HOLOCL strengthens a crucial part of the uml to an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

September 2007

638 pages

ISBN:9781595938114

DOI:10.1145/1287624

General Chair:
Ivica Crnkovic
Mälardalen University, Sweden
,
Program Chair:
Antonia Bertolino
ISTI-CNR, Italy

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 September 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ESEC/FSE07

Sponsor:

ESEC/FSE07: Joint 11th European Software Engineering Conference 2007

September 3 - 7, 2007

Dubrovnik, Croatia

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
315
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Marussy KSemerath OVarro D(2022)Automated Generation of Consistent Graph Models With Multiplicity ReasoningIEEE Transactions on Software Engineering10.1109/TSE.2020.302573248:5(1610-1629)Online publication date: 1-May-2022
https://doi.org/10.1109/TSE.2020.3025732
Clariso RGonzalez CCabot J(2019)Smart Bound Selection for the Verification of UML/OCL Class DiagramsIEEE Transactions on Software Engineering10.1109/TSE.2017.277783045:4(412-426)Online publication date: 1-Apr-2019
https://doi.org/10.1109/TSE.2017.2777830
Chavez HShen WFrance RMechling BLi G(2016)An Approach to Checking Consistency between UML Class Model and Its Java ImplementationIEEE Transactions on Software Engineering10.1109/TSE.2015.248864542:4(322-344)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1109/TSE.2015.2488645
Clarisó RGonzález CCabot J(2015)Towards Domain Refinement for UML/OCL Bounded VerificationSoftware Engineering and Formal Methods10.1007/978-3-319-22969-0_8(108-114)Online publication date: 21-Aug-2015
https://doi.org/10.1007/978-3-319-22969-0_8
González CBüttner FClarisó RCabot JGnesi SGruner SPlat NRumpe B(2012)EMFtoCSPProceedings of the First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches10.5555/2663689.2663697(44-50)Online publication date: 2-Jun-2012
https://dl.acm.org/doi/10.5555/2663689.2663697
Gonzalez CButtner FClariso RCabot J(2012)EMFtoCSP: A tool for the lightweight verification of EMF models2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA)10.1109/FormSERA.2012.6229788(44-50)Online publication date: Jun-2012
https://doi.org/10.1109/FormSERA.2012.6229788
Tan LYang ZXie J(2010)OCL constraints automatic generation for UML class diagram2010 IEEE International Conference on Software Engineering and Service Sciences10.1109/ICSESS.2010.5552361(392-395)Online publication date: Jul-2010
https://doi.org/10.1109/ICSESS.2010.5552361
Bajwa IBordbar BLee M(2010)OCL Constraints Generation from Natural Language SpecificationProceedings of the 2010 14th IEEE International Enterprise Distributed Object Computing Conference10.1109/EDOC.2010.33(204-213)Online publication date: 25-Oct-2010
https://dl.acm.org/doi/10.1109/EDOC.2010.33

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Verification-driven slicing of UML/OCL models

Transformation of TOCL temporal properties into OCL

HOL-OCL: a formal proof environment for UML/OCL