A combined method for verification of large-scale data models
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, declarati...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/797 |
| _version_ | 1828844652714786816 |
|---|---|
| author | V. A. Semenov S. V. Morozov D. V. Ilyin |
| author_facet | V. A. Semenov S. V. Morozov D. V. Ilyin |
| author_sort | V. A. Semenov |
| collection | DOAJ |
| description | 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). |
| first_indexed | 2024-12-12T21:11:05Z |
| format | Article |
| id | doaj.art-74d912d277834b8da7ff0fa662539bb9 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-12T21:11:05Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-74d912d277834b8da7ff0fa662539bb92022-12-22T00:11:54ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0126219723010.15514/ISPRAS-2014-26(2)-9797A combined method for verification of large-scale data modelsV. A. Semenov0S. V. Morozov1D. V. Ilyin2ИСП РАН, МоскваИСП РАН, МоскваИСП РАН, Москва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).https://ispranproceedings.elpub.ru/jour/article/view/797верификация моделей, объектно-ориентированное моделирование, uml/ocl, express, логическое программирование в ограничениях, линейное целочисленное программирование, семантическая реконсиляция |
| spellingShingle | V. A. Semenov S. V. Morozov D. V. Ilyin A combined method for verification of large-scale data models Труды Института системного программирования РАН верификация моделей, объектно-ориентированное моделирование, uml/ocl, express, логическое программирование в ограничениях, линейное целочисленное программирование, семантическая реконсиляция |
| title | A combined method for verification of large-scale data models |
| title_full | A combined method for verification of large-scale data models |
| title_fullStr | A combined method for verification of large-scale data models |
| title_full_unstemmed | A combined method for verification of large-scale data models |
| title_short | A combined method for verification of large-scale data models |
| title_sort | combined method for verification of large scale data models |
| topic | верификация моделей, объектно-ориентированное моделирование, uml/ocl, express, логическое программирование в ограничениях, линейное целочисленное программирование, семантическая реконсиляция |
| url | https://ispranproceedings.elpub.ru/jour/article/view/797 |
| work_keys_str_mv | AT vasemenov acombinedmethodforverificationoflargescaledatamodels AT svmorozov acombinedmethodforverificationoflargescaledatamodels AT dvilyin acombinedmethodforverificationoflargescaledatamodels AT vasemenov combinedmethodforverificationoflargescaledatamodels AT svmorozov combinedmethodforverificationoflargescaledatamodels AT dvilyin combinedmethodforverificationoflargescaledatamodels |