Asadullah Shaikh
Robert Clarisó
Uffe Kock Wiil
ABSTRACT
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 check the correctness of a model, but their high computational complexity can limit their scalability. In this paper, we consider a specific static model (UML class diagrams annotated with unrestricted OCL constraints) and a specific property to verify (satisfiability, i.e., "is it possible to create objects without violating any constraint?"). Current approaches to this problem have an exponential worst-case runtime. We propose a technique to improve their scalability by partitioning the original model into submodels (slices) which can be verified independently and where irrelevant information has been abstracted. The definition of the slicing procedure ensures that the property under verification is preserved after partitioning.
- }}M. Balaban and A. Maraee. A UML-based method for deciding finite satisfiability in Description Logics. In DL'2008, volume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.Google Scholar
- }}D. Berardi, D. Calvanese, and G. D. Giacomo. Reasoning on UML class diagrams. AIntelligence, 168:70--118, 2005. Google ScholarDigital Library
- }}A. D. Brucker and B. Wolff. The HOL-OCL book. Technical Report 525, ETH Zurich, 2006.Google Scholar
- }}J. Cabot, R. Clarisó, and D. Riera. UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming. In ASE'2007, pages 547--548. ACM, 2007. Google ScholarDigital Library
- }}J. Conesa and A. Olivé. Pruning ontologies in the development of conceptual schemas of information systems. In ER'2004, volume 3288 of LNCS, pages 122--135. Springer, 2004.Google ScholarCross Ref
- }}DBLP. Digital bibliography andy library project. http://guifre.lsi.upc.edu/DBLP.pdf.Google Scholar
- }}V. Durairaj and P. Kalla. Guiding CNF-SAT search via efficient constraint partitioning. In ICCAD'04, pages 498--501. IEEE Computer Society, 2004. Google ScholarDigital Library
- }}M. Gogolla, J. Bohling, and M. Richters. Validating UML and OCL models in USE by automatic snapshot generation. Journal on Software and System Modeling, 4(4):386--398, 2005.Google ScholarCross Ref
- }}M. Gogolla and M. Richters. Expressing UML Class Diagrams Properties with OCL. In AOM with the OCL, volume 2263 of LNCS, pages 86--115. Springer, 2001. Google ScholarDigital Library
- }}D. Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, 11(2):256--290, 2002. Google ScholarDigital Library
- }}D. Jackson. Software Abstractions: Logic, Language and Analysis. MIT Press, 2006. Google ScholarDigital Library
- }}H. H. Kagdi, J. I. Maletic, and A. Sutton. Context-free slicing of UML class models. In ICSM'05, pages 635--638. IEEE Computer Society, 2005. Google ScholarDigital Library
- }}T. H. Kim, Y. T. Song, L. Chung, and D. Huynh. Software architecture analysis: A dynamic slicing approach. International Journal of Computer & Information Science, 1(2):91--103, 2000. Google ScholarDigital Library
- }}R. Kollmann and M. Gogolla. Metric-based selective representation of uml diagrams. In CSMR'02, pages 89--98. IEEE Computer Society, 2002. Google ScholarDigital Library
- }}J. T. Lallchandani and R. Mall. Slicing UML architectural models. In ACM / SIGSOFT SEN, volume 33, pages 1--9, 2008. Google ScholarDigital Library
- }}Y. C. Law and J. H. Lee. Symmetry breaking constraints for value symmetries in constraint satisfaction. Constraints, 11(2--3):221--267, 2006. Google ScholarDigital Library
- }}A. Maraee and M. Balaban. Efficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets. In ECMDA-FA'2007, volume 4530 of LNCS, pages 17--31. Springer, 2007. Google ScholarDigital Library
- }}B. J. Peterson, W. A. Andersen, and J. Engel. Knowledge bus: Generating application-focused databases from large ontologies. In KRDB '98, volume 10 of CEUR Workshop Proceedings, pages 2.1--2.10. CEUR-WS.org, 1998.Google Scholar
- }}A. Queralt and E. Teniente. Reasoning on UML class diagrams with OCL constraints. In ER'2006, volume 4215 of LNCS, pages 497--512. Springer-Verlag, 2006. Google ScholarDigital Library
- }}G. Rull, C. Farré, E. Teniente, and T. Urpí. Computing explanations for unlively queries in databases. In CIKM'07, pages 955--958. ACM, 2007. Google ScholarDigital Library
- }}J. A. Stafford, D. J. Richardson, and A. L. Wolf. Architecture-level dependence analysis in support of software maintenance. In ISAW'98, pages 129--132, 1998. Google ScholarDigital Library
- }}B. Swartout, P. Ramesh, K. Knight, and T. Russ. Toward distributed use of large-scale ontologies. AAAI Symp. on Ontological Engineering, pages 138--148, 1997.Google Scholar
- }}F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.Google Scholar
- }}E. Uzuncaova and S. Khurshid. Kato: A program slicing tool for declarative specifications. In ICSE '07, pages 767--770. IEEE Computer Society, 2007. Google ScholarDigital Library
- }}M. Weiser. Program slicing. IEEE Trans. Software Eng., 10(4):352--357, 1984.Google ScholarDigital Library
Index Terms
- Verification-driven slicing of UML/OCL models
Recommendations
Slicing UML-based Models of Real-time Embedded Systems
MODELS '18: Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and SystemsModels of Real-time Embedded (RTE) systems may encompass many components with often many different kinds of dependencies describing, e.g., structural relationships or the flow of data, control, or messages. Understanding and properly accounting for them ...
Behavior Modeling with Interaction Diagrams in a UML and OCL Tool
BM-FA '14: Proceedings of the 2014 Workshop on Behaviour Modelling-Foundations and ApplicationsThis contribution discusses system modeling with UML behavior diagrams. We consider statecharts and both kinds of interaction diagrams, i.e., sequence and communication diagrams. We present new implementation features in a UML and OCL modeling tool: (1) ...
Constraint-driven development
To obtain the full benefits of model-driven development (MDD) approaches such as MDA, a suitable level of abstraction needs to be chosen which enables the core functionality and properties of a system to be expressed, independent of programming language ...
Comments