Methods and Means for Automated Information Systems Development based on Ontology «Software and Hardware Complexes Quality Management»

The paper presents development and verification methods and means of requirements and design solutions formal models. They are intended to create complex critical automated information systems in a same model-language and information-software environment for all its participants. The development and verification processes are carried out in an automated way on the basis of subject-oriented ontologies. Ontologies describe the quality management processes of software and hardware complexes at the stages of requirements justification and system design. They are developing by means modeling and design languages SysML, FUML, OCL structures and mechanisms, the Petri nets mathematical apparatus, time automata and time logics. In order to execute of validation and verification for complex of requirements and design solutions, construction and model execution route analysis algorithms in the VM FUML virtual machine environment are developed.  Integration and use methods for specialized verification tools CPN Tools, Rodin, SPIN and Modelica as means to automated testing of complex requirements and design solutions models are proposed.  This complex provides more effective interaction between the customer and the contractor both in the development of requirements and in the design of the system, along with this, detection and provides limination of defects through the automated verification, validation and correction procedures implementation. This approach application will improve the quality of requirements and design solutions, as well as improve economic performance by reducing the financial and time costs,  which associated with the implementation of additional work in the case of defects, and when changing requirements or operating conditions.

1. The Standish Group report. URL: https://www.standishgroup.com/store/services/10-chaos-report-decision-latency-theory-2018-package.html, accessed 21.05.2019.

2. Systems Engineering and Software Engineering [online]. URL: https://www.sebokwiki.org/wiki/Systems_Engineering_and_Software_Engineering, accessed 25.05.2019.

3. Laura E. Hart. Introduction To Model-Based System Engineering (MBSE) and SysML [online]. URL: https://www.incose.org/docs/default-source/delaware-valley/mbse-overview-incose-30-july-2015.pdf, accessed 21.05.2019.

4. Ковалёв С.П. Теоретико-категорный подход к метапрограммированию. М.: ИПУ РАН, 2014, 112 стр./ S.P. Kovalev. Category-theoretic approach to metaprogramming. M.: ICS RAS, 2014, 112 p. (in Russian).

5. Ковалeв С.П. Теоретико-категорный подход к проектированию программных систем. Фундаментальная и прикладная математика, том 19, вып. 3, 2014 г., стр. 111–170 / Kovalev S.P. Category-theoretic approach to the design of software systems. Fundamental and Applied Mathematics, vol. 19, issue 3, 2014, pp. 111-170 (in Russian).

6. Peter H. Feiler, David P. Gluch. Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language. Addison-Wesley Professional, 2012, 479 p.

7. Д.В. Буздалов, С.В. Зеленов, Е.В. Корныхин, А.К. Петренко, А.В. Страх, А.А. Угненко, А.В. Хорошилов. Инструментальные средства проектирования систем интегрированной модульной авионики. Труды ИСП РАН, том 26, вып. 1, 2014 г., стр. 201-230 / D.V. Buzdalov, S.V. Zelenov, E.V. Kornykhin, A.K. Petrenko, A.V. Strakh, A.A. Ugnenko, A.V. Khoroshilov. Design tools for integrated modular avionics systems. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 201-230 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-6.

8. Зеленов С.В., Зеленова С.А. Моделирование программно-аппаратных систем и анализ их безопасности. Труды ИСП РАН, том 29, вып. 5, 2017 г., стр. 257-282 / S.V Zelenov, S.A. Zelenova Modeling of software and hardware systems and analysis of their safety. Trudy ISP RAN/Proc. ISP RAS, vol. 29, vol. 5, 2017, pp. 257-282 (in Russian). DOI: 10.15514/ISPRAS-2017-29(5)-13

9. An Orchestrated Survey on Automated Software Test Case Generation. Journal of Systems and Software, vol. 86, issue 8, 2013, pp. 1978-2001.

10. Photchana Sawprakhon, Yachai Limpiyakorn. Sequence Diagram Generation with Model Transformation Technology. In Proc. of the International MultiConference of Engineers and Computer Scientists, 2014, pp. 584-589.

11. Thomas Buchmann and Alexander Rimer. Unifying Modeling and Programming with ALF. In Proc. of the Second International Conference on Advances and Trends in Software Engineering, 2016, pp. 10-15.

12. Li S., Balaguer S., David A. et al. Scenario-based verification of real-time systems using Uppaal. Formal Methods in System Design, vol. 37, Issue 2–3, 2010, pp 200–264.

13. Ермакова В.О., Ломазова И.А. Трансляция вложенных сетей Петри в классические сети Петри для верификации разверток. Труды ИСП РАН, том 28, вып, 4, 2016, стр. 115-136 / Ermakova V.O., Lomazova I.A. Translation of Nested Petri Nets into Petri Nets for Unfoldings Verification. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 4, 2016, pp. 115-136 (in Russian). DOI: 10.15514/ISPRAS-2016-28(4)-7.

14. Девянин П.Н., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Сравнение способов декомпозиции спецификаций на Event-B. Программирование, том 42, № 4, 2016 г., стр. 17-26 / Comparison of specification decomposition methods in Event-B Devyanin P.N., Kulyamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Programming and Computer Software, vol. 42, № 4, 2016, pp. 198-205.

15. Самонов А.В., Самонова Г.Н. Методика и средства разработки и верификации формальных FUML моделей требований и архитектуры сложных программно-технических систем. Труды ИСП РАН, том 30, вып. 5, 2018, стр. 125-148 / Samonov A.V., Samonova G.N. Methodology and Tools for Development and Verification of formal fUML models of Requirements and Architecture for complex software and hardware systems. Trudy ISP RAN/Proc. ISP RAS, 2018, vol. 30, issue 5, pp.125-148. DOI: 10.15514/ISPRAS-2018-30(5)-8.

16. Eclipse GEMOC Studio [online]. URL: https://projects.eclipse.org/projects/modeling.gemoc, accessed 20.06 2019.

17. Meyers B., Deshayes R., Lucio L., Syriani E., Vangheluwe H., Wimmer M. ProMoBox: A Framework for Generating Domain-Specific Property Languages. Lecture Notes in Computer Science, vol. 8706, 2014, pp. 1-20.

18. Bousse E., Mayerhofer T., Combemale B., Baudry B. Advanced and efficient execution trace management for executable domain-specific modeling languages. Software & Systems Modeling, vol. 18, issue 1, 2019, pp 385–421.

19. CPN Tools Homepage. CPN Tools is a tool for editing, simulating, and analyzing Colored Petri nets URL: http://cpntools.org/, accessed 27.05.2019.

20. Rodin. URL: http://www.event-b.org/, accessed 11.05.2019.

21. SPIN. URL: http://spinroot.com/spin/whatispin.html, accessed 11.06.2019.

22. Ю.Г. Карпов, И.В. Шомшина. Введение в язык Promela и систему комплексной верификации Spin: учебное пособие. Изд-во Политехнического ун-та, 2010, 110 стр. / Y.G. Karpov, I.V. Shamshina. Introduction to the language Promela and the verification system of the comprehensive Spin: a training manual. Publishing house of Polytechnic University, 2010, 110 p. (in Russian).

23. Timed Automata: Semantics, Algorithms and Tools. Johan Bengtsson and Wang Yi. Lecture Notes in Computer Science, vol. 3098, 2003, pp. 87-124.

24. Твардовский А.С., Лапутенко А.В. О возможностях автоматного описания параллельной композиции временных автоматов. Труды ИСП РАН, том 30, вып. 1, 2018 г., стр. 25-40. / A.S Twardowski., AV. Lopotenco. On the possibilities of automaton description of parallel composition of time automata. Trudy ISP RAN/Proc. ISP RAS, volume 30, vol. 1, 2018, pp. 25-40 (in Russian). DOI: 10.15514/ISPRAS-2018-30(1)-2.

25. Openmodelica. URL: https://www.openmodelica. org/, accessed 27.05.2019.