Preview

Труды Института системного программирования РАН

Расширенный поиск

Комбинированный метод верификации масштабных моделей данных

https://doi.org/10.15514/ISPRAS-2014-26(2)-9

Аннотация

Статья адресована актуальной проблеме верификации масштабных моделей данных, применяемых в различных индустриальных областях и специфицируемых на популярных универсальных объектно-ориентированных языках, таких как EXPRESS, UML/OCL. Основные преимущества языков информационного моделирования (высокая выразительность, декларативность, богатство синтаксических конструкций) отрицательно сказываются в процессе автоматической верификации спецификаций. Существующие методы верификации моделей вследствие высокой вычислительной сложности не могут использоваться для решения данной проблемы. В статье предлагается комбинированный метод верификации объектно-ориентированных моделей данных, основанный на последовательной редукции к нескольким постановкам математических задач: линейного программирования, удовлетворения ограничений (CSP), выполнимости булевых формул (SAT). Детально исследуется ключевая проблема определения необходимого количества экземпляров для генерации корректной коллекции объектов и ее редукция к задаче целочисленного линейного программирования. Работа поддержана РФФИ (грант 13-07-00390).

Об авторах

В. А. Семенов
ИСП РАН, Москва
Россия


С. В. Морозов
ИСП РАН, Москва
Россия


Д. В. Ильин
ИСП РАН, Москва
Россия


Список литературы

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. Чен П. Модель «сущность-связь» - шаг к единому представлению о данных. // СУБД, № 3, 1995. http://www.osp.ru/dbms/1995/03/271.htm

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, 14(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, 11(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, 168(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, 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, 4(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. Семенов В.А., Морозов С.В., Тарлапан О.А. Инкрементальная верификация объектно-ориентированных данных на основе спецификации ограничений. // Труды Института системного программирования / под ред. В.П. Иванникова, т.8, ч.2, 2004, с. 21-52.

39. Семенов В.А., Ерошкин С.Г., Караулов А.А., Энкович И.В. Семантическая реконсиляция прикладных данных на основе моделей. // Труды Института системного программирования / под ред. В.П. Иванникова, т.13, ч.2, 2007, с. 141-164.

40. Vanderbei R.J. Linear Programming. Foundations and Extensions. Third edition. Princeton University, 2008.

41. Шевченко В.Н., Золотых Н.Ю. Линейное и целочисленное линейное программирование. - Нижний Новгород: издательство Нижегородского госуниверситета им. Н.И. Лобачевского, 2004.

42. Карманов В.Г. Математическое программирование: учебное пособие. 5-е издание. - М.: Физматлит, 2004.

43. 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).

44. 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).

45. 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).

46. Karmanov V.G. Matematicheskoe programmirovanie: uchebnoe posobie. 5-e izdanie [Mathematical programming: a tutorial. Fifth edition]. Moscow, Fizmatlit Publ., 2004 (in Russian).


Рецензия

Для цитирования:


Семенов В.А., Морозов С.В., Ильин Д.В. Комбинированный метод верификации масштабных моделей данных. Труды Института системного программирования РАН. 2014;26(2):197-230. https://doi.org/10.15514/ISPRAS-2014-26(2)-9

For citation:


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



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)