research-article

Towards automatic determination of problem bounds for object instantiation in static model verification

Authors:

Mathias Soeken,

Robert Wille,

Rolf DrechslerAuthors Info & Claims

MoDeVVa: Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation

Article No.: 2, Pages 1 - 4

https://doi.org/10.1145/2095654.2095657

Published: 17 October 2011 Publication History

Get Access

Abstract

The application of formal methods in the detection of inconsistencies and design flaws within models has been intensely studied in recent years. Since consistency checking is in principle undecidable due to the infinite number of possible system states, problem bounds have to be defined making the analysis tractable. However, defining these problem bounds requires detailed design knowledge and, thus, impedes an automatic verification flow.

In this paper, we present first ideas and results of how to automatically determine valid problem bounds for consistency checking algorithms. For this purpose, we make use of automatic proof engines for linear integer arithmetic. We describe the approach by means of class diagrams given in the Unified Modeling Language (UML) extended by constraints given in the Object Constraint Language (OCL).

References

[1]

K. Anastasakis, B. Bordbar, G. Georg, and I. Ray. UML2Alloy: A Challenging Model Transformation. In Int'l Conf. on Model Driven Engineering Languages and Systems, pages 436--450. Springer, Oct. 2007.

Digital Library

Google Scholar

[2]

J. Cabot, R. Clarisó, and D. Riera. Verification of UML/OCL Class Diagrams using Constraint Programming. In IEEE Int'l. Conf. on Software Testing Verification and Validation Workshop, pages 73--80, Apr. 2008.

Digital Library

Google Scholar

[3]

J. Cabot, R. Clarisó, and D. Riera. Verifying UML/OCL Operation Contracts. In M. Leuschel and H. Wehrheim, editors, Integrated Formal Methods, volume 5423 of Lecture Notes in Computer Science, pages 40--55. Springer, Feb. 2009.

Digital Library

Google Scholar

[4]

B. Dutertre and L. M. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In T. Ball and R. B. Jones, editors, Int'l Conf. on Computer Aided Verification, volume 4144 of Lecture Notes in Computer Science, pages 81--94. Springer, Aug. 2006.

Digital Library

Google Scholar

[5]

M. Gogolla, F. Büttner, and M. Richters. USE: A UML-based specification environment for validating UML and OCL. Science of Computer Programming, 69(1--3):27--34, 2007.

Digital Library

Google Scholar

[6]

M. Gogolla, M. Kuhlmann, and L. Hamann. Consistency, Independence and Consequences in UML and OCL Models. In Tests and Proofs, pages 90--104. Springer, July 2009.

Digital Library

Google Scholar

[7]

M. Gogolla and M. Richters. Expressing UML Class Diagrams Properties with OCL. In T. Clark and J. Warmer, editors, Object Modeling with the OCL, volume 2263 of Lecture Notes in Computer Science, pages 85--114. Springer, 2002.

Digital Library

Google Scholar

[8]

D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA, USA, Apr. 2006.

Digital Library

Google Scholar

[9]

M. Kuhlmann, L. Hamann, and M. Gogolla. Extensive Validation of OCL Models by Integrating SAT Solving into USE. In Int'l. Conf. on Objects, Models, Components, Patterns, volume 6705 of Lecture Notes in Computer Science, pages 290--306. Springer, June 2011.

Digital Library

Google Scholar

[10]

J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language reference manual. Addison-Wesley Longman, Essex, UK, Jan. 1999.

Digital Library

Google Scholar

[11]

M. Soeken, R. Wille, and R. Drechsler. Verifying Dynamic Aspects of UML Models. In Design, Automation and Test in Europe, pages 1077--1082. IEEE Computer Society, Mar. 2011.

Google Scholar

[12]

M. Soeken, R. Wille, M. Kuhlmann, M. Gogolla, and R. Drechsler. Verifying UML/OCL models using Boolean satisfiability. In Design, Automation and Test in Europe, pages 1341--1344. IEEE Computer Society, Mar. 2010.

Digital Library

Google Scholar

[13]

E. Torlak and D. Jackson. Kodkod: A Relational Model Finder. In TACAS, volume 4424 of Lecture Notes in Computer Science, pages 632--647. Springer, Apr. 2007.

Digital Library

Google Scholar

[14]

J. Warmer and A. Kleppe. The Object Constraint Language: Precise modeling with UML. Addison-Wesley Longman, Boston, MA, USA, Mar. 1999.

Digital Library

Google Scholar

Cited By

View all

Wu HFarrell M(2021)A formal approach to finding inconsistencies in a metamodelSoftware and Systems Modeling10.1007/s10270-020-00849-8Online publication date: 29-Jan-2021
https://doi.org/10.1007/s10270-020-00849-8
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
Przigoda NWille RPrzigoda JDrechsler RPrzigoda NWille RPrzigoda JDrechsler R(2018)Re-utilizing Verification Results of UML/OCL ModelsAutomated Validation & Verification of UML/OCL Models Using Satisfiability Solvers10.1007/978-3-319-72814-8_8(201-233)Online publication date: 17-Jan-2018
https://doi.org/10.1007/978-3-319-72814-8_8
Show More Cited By

Index Terms

Recommendations

Semi-automatic generation of metamodels from model sketches
ASE '13: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering

Traditionally, metamodeling is an upfront activity performed by experts for defining modeling languages. Modeling tools then typically restrict modelers to using only constructs defined in the metamodel. This is inappropriate when users want to sketch ...
A UML-based static verification framework for security
Special Issue on RE'09: Security Requirements Engineering; Guest Editors: Eric Dubois and Haralambos Mouratidis

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages ...
Domain-specific model verification with QVT
ECMFA'11: Proceedings of the 7th European conference on Modelling foundations and applications

Model verification is the process of checking models for known problems (or anti-patterns). We propose a new approach to declaratively specify and automatically detect problems in domain-specific models using QVT (Query/View/Transformation). Problems ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

MoDeVVa: Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation

October 2011

62 pages

ISBN:9781450309141

DOI:10.1145/2095654

Editors:
Stephan Weißleder
Fraunhofer FIRST/HU Berlin, Germany
,
Levi Lúcio
McGill University, Canada
,
Harald Cichos
TÜ Darmstadt, Germany
,
Frédéric Fondement
Université de Haute Alsace, France

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: 17 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

MoDeVVa '11

MoDeVVa '11: Model-Driven Engineering, Verification, and Validation

October 17, 2011

Wellington, New Zealand

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
106
Total Downloads

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

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Wu HFarrell M(2021)A formal approach to finding inconsistencies in a metamodelSoftware and Systems Modeling10.1007/s10270-020-00849-8Online publication date: 29-Jan-2021
https://doi.org/10.1007/s10270-020-00849-8
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
Przigoda NWille RPrzigoda JDrechsler RPrzigoda NWille RPrzigoda JDrechsler R(2018)Re-utilizing Verification Results of UML/OCL ModelsAutomated Validation & Verification of UML/OCL Models Using Satisfiability Solvers10.1007/978-3-319-72814-8_8(201-233)Online publication date: 17-Jan-2018
https://doi.org/10.1007/978-3-319-72814-8_8
Przigoda NWille RPrzigoda JDrechsler RPrzigoda NWille RPrzigoda JDrechsler R(2018)A Symbolic Formulation for ModelsAutomated Validation & Verification of UML/OCL Models Using Satisfiability Solvers10.1007/978-3-319-72814-8_3(25-94)Online publication date: 17-Jan-2018
https://doi.org/10.1007/978-3-319-72814-8_3
Soeken MDrechsler RSoeken MDrechsler R(2014)Verification of Static AspectsFormal Specification Level10.1007/978-3-319-08699-6_4(57-108)Online publication date: 10-Oct-2014
https://doi.org/10.1007/978-3-319-08699-6_4

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

Semi-automatic generation of metamodels from model sketches

A UML-based static verification framework for security

Domain-specific model verification with QVT