Комбинированный метод верификации масштабных моделей данных
https://doi.org/10.15514/ISPRAS-2014-26(2)-9
Аннотация
Об авторах
В. А. СеменовРоссия
С. В. Морозов
Россия
Д. В. Ильин
Россия
Список литературы
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