A combined method for verification of large-scale data models
https://doi.org/10.15514/ISPRAS-2014-26(2)-9
Abstract
The paper is addressed to the actual problem of verification of large-scale data models applied in various industrial areas and specified using popular general-purpose object-oriented languages, such as EXPRESS, UML/OCL. Main benefits of information modeling languages (high expressiveness, declarative nature, advanced set of syntactic units) negatively affect the process of automatic verification of the specifications. The known approaches are based on reduction of the original complex problem to some well-known mathematical statement and its solution by existing methods. The performed analytical survey of the existing methods for model verification demonstrates that they cannot be used for solving the problem because of their high computational complexity. A combined method for verification of large-scale data models is proposed in the paper. The method is based on sequential reduction to the several mathematical problem statements: linear programming, constraint satisfaction problem (CSP), Boolean satisfiability (SAT). Usage of the combined method allows to avoid efficiency issues peculiar to the known approaches. At the first step the polynomial complexity methods of integer linear programming are applied to the original large-scale problem and localize the search region for solution by detection of the necessary amount of objects. At the next steps constraints imposed onto relatively small groups of objects can be considered individually, which allows to reduce significantly dimension of the problem. The key problem of estimation of the number of instances intended for generation of correct object collection and its reduction to an integer linear programming problem is investigated in detail. The performed experiments demonstrate prospectivity of the combined computational strategy and efficiency of the proposed method for verification of large-scale data models. The work is supported by RFBR (grant 13-07-00390).
About the Authors
V. A. Semenov
ISP RAS, Moscow
Russian Federation
Russian Federation
S. V. Morozov
ISP RAS, Moscow
Russian Federation
Russian Federation
D. V. Ilyin
ISP RAS, Moscow
Russian Federation
Russian Federation
References
1. Model Driven Architecture: The Architecture of Choice for a Changing World. Executive Overview, October 2013. http://www.omg.org/mda/executive_overview.htm
2. Calafat A.Q. Validation of UML Conceptual Schemas with OCL Constraints and Operators. PhD Thesis, adviced by Dr. E. Teniente, Universitat Politecnica de Catalunya, Barcelona, 2009.
3. ISO 10303-11:2004. Industrial automation systems and integration — Product data representation and exchange — Part 11: Description methods: The EXPRESS language reference manual.
4. Unified Modeling Language (UML), V2.4.1, Release Date: August 2011. http://www.omg.org/spec/UML/2.4.1
5. Object Constraint Language (OCL), V2.3.1, Release Date: January 2012. http://www.omg.org/spec/OCL/2.3.1
6. IFC4 Release Summary, March 2013. http://www.buildingsmart-tech.org/specifications/ifc-releases/ifc4-release/ifc4-release-summary
7. Khemlani L. The CIS/2 Format: Another AEC Interoperability Standard. AECbytes Newsletter, July 27, 2005. http://www.aecbytes.com/buildingthefuture/2005/CIS2format.html
8. ISO 10303-1:1994. Industrial automation systems and integration — Product data representation and exchange — Part 1: Overview and fundamental principles.
9. ISO 15926-1:2004. Industrial automation systems and integration — Integration of life-cycle data for process plants including oil and gas production facilities — Part 1: Overview and fundamental principles.
10. Chen P. The entity-relationship model — toward a unified view of data. ACM Transactions on Database Systems, vol. 1, no. 1, 1976, pp. 9–36.
11. Alloy 4: a language & tool for relational models, 2012. http://alloy.mit.edu/alloy
12. Formica A. Finite Satisfiability of Integrity Constraints in Object-Oriented Database Schemas. IEEE Transactions on Knowledge and Data Engineering, vol. 14, no. 1, 2002, pp. 123–139.
13. Baader F., et al. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, 2003.
14. Lenzerini M., Nobili P. On the Satisfiability of Dependency Constraints in Entity-Relationship Schemata. Proceedings of the 13th VLDB Conference, 1987, pp. 147–154.
15. Maraee A., Balaban M. Efficient Reasoning about Finite Satisfiability of UML Class Diagrams with Constrained Generalization Sets. LNCS 4530, Proceedings of European Conference on Model Driven Architecture — Foundations and Applications, 2007, pp. 17–31.
16. Jackson D. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, vol. 11, no. 2, 2002, pp. 266–290.
17. Anastasakis K., Bordbar B., Georg G., Ray I. UML2Alloy: A challenging model transformation. LNCS 4735, Model Driven Engineering Languages and Systems, 2007, pp. 436–450.
18. Ramirez A., Vanpeperstraete P., Rueckert A., Odutola K., Bennett J., Tolke L., van der Wulp W. ArgoUML User Manual: A tutorial and reference description, 2011. http://argouml.tigris.org/ documentation/manual-0.34
19. Soeken M., Wille R., Kuhlmann M., Gogolla M., Drechsler R. Verifying UML/OCL Models Using Boolean Satisfiability. Design, Automation & Test in Europe Conference & Exhibition (DATE), 2010, pp. 1341–1344.
20. Turhan A.Y. Description Logic Reasoning for Semantic Web Ontologies. WIMS’11 Proceedings of the International Conference on Web Intelligence, Mining and Semantics, Article 6, 2011.
21. Berardi D., Calvanese D., de Giacomo G. Reasoning on UML Class Diagrams. Artificial Intelligence, vol. 168, no 1–2, 2005, pp. 70–118.
22. The FaCT System, April 2003. http://www.cs.man.ac.uk/~horrocks/FaCT
23. Haarslev V., Möller R. RACER system description. LNAI 2083, Automated Reasoning, 2001, pp. 701–705.
24. van der Straeten R., Mens T., Simmonds J., Jonckers V. Using Description Logic to Maintain Consistency between UML Models. LNCS 2863, The Unified Modeling Language. Modeling Languages and Applications, 2003, pp. 326–340.
25. Loom Project Home Page, July 2007. http://www.isi.edu/isd/LOOM
26. PVS Specification and Verification System, January 2013. http://pvs.csl.sri.com
27. Kyas M., Fecher H., de Boer F.S., Jacob J., Hooman J., van der Zwaag M., Arons T., Kugler H. Formalizing UML Models and OCL Constraints in PVS. Electronic Notes in Theoretical Computer Science, vol. 115, 2005, pp. 39–47.
28. Brucker A.D., Wolff B. The HOL-OCL book. Technical Report 525, ETH Zurich, 2006.
29. Nipkow T., Paulson L.C., Wenzel M. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS 2283, 2002.
30. Tsang E. Foundations of constraint satisfaction. Academic Press Limited, London & San-Diego, 1993.
31. Cabot J., Clariso R., Riera D. UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming. Proceedings of the 22nd ACM/IEEE International Conference on Automated Software Engineering (ASE ’07), 2007, pp. 547–548.
32. Cabot J., Clariso R., Riera D. Verification of UML/OCL Class Diagrams using Constraint Programming. Proceedings of the IEEE International Conference on Software Testing Verification and Validation Workshop (ICSTW’08), 2008, pp. 73–80.
33. Apt K.R., Wallace M.G. Constraint Logic Programming using ECLiPSe. Cambridge University Press, 2007.
34. Gogolla M., Bohling J., Richters M. Validating UML and OCL models in USE by automatic snapshot generation. Software & System Modeling, vol. 4, no. 4, 2005, pp. 386–398.
35. Shaikh A., Wiil U.K., Memon N. Evaluation of Tools and Slicing Techniques for Efficient Verification of UML/OCL Class Diagrams. Advances in Software Engineering, 2011, Article ID 370198, 18 p.p.
36. Breu R., Hinkel U., Hofmann C., Klein C., Paech B., Rumpe B., Thurner V. Towards a Formalization of the Unified Modeling Language. LNCS 1241, ECOOP’97 — Object-Oriented Programming, 1997, pp. 344–366.
37. Richters M., Gogolla M. On Formalizing the UML Object Constraint Language OCL. LNCS 1507, Conceptual Modeling — ER’98, 1998, pp. 449–464.
38. Semenov V.A., Morozov S.V., Tarlapan O.A. Inkremental'naya verifikatsiya ob'ektno-orientirovannyh dannyh na osnove spetsifikatsii ogranichenij [Incremental verification of object-oriented data based on specification of constraints]. Trudy ISP RAN [The Proceedings of ISP RAS], vol. 8, no. 2, 2004, pp. 21–52 (in Russian).
39. Semenov V.A., Eroshkin S.G., Karaulov A.A., Enkovich I.V. Semanticheskaya rekonsilyatsiya prikladnyh dannyh na osnove modelej [Model-based semantic reconciliation of applied data]. Trudy ISP RAN [The Proceedings of ISP RAS], vol. 13, no. 2, 2007, pp. 141–164 (in Russian).
40. Vanderbei R.J. Linear Programming. Foundations and Extensions. Third edition. Princeton University, 2008.
41. Shevchenko V.N., Zolotyh N.Yu. Linejnoe i tselochislennoe linejnoe programmirovanie [Linear and integer linear programming]. Nizhniy Novgorod, N.I. Lobachevskiy State University Publ., 2004 (in Russian).
42. Karmanov V.G. Matematicheskoe programmirovanie: uchebnoe posobie. 5-e izdanie [Mathematical programming: a tutorial. Fifth edition]. Moscow, Fizmatlit Publ., 2004 (in Russian).
Review
For citations:
Semenov V.A., Morozov S.V., Ilyin D.V. A combined method for verification of large-scale data models. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2014;26(2):197-230. (In Russ.) https://doi.org/10.15514/ISPRAS-2014-26(2)-9
Email this article 