Методика и средства разработки и верификации формальных fUML моделей требований и архитектуры сложных программно-технических систем

В статье представлены модели и алгоритмы обеспечения сквозного контроля качества сложных программно-технических систем (СПТС) посредством реализации программно-управляемого процесса разработки и верификации формальных моделей требований и архитектуры СПТС. Дан анализ научных публикаций и нормативно-методической базы в области разработки и применения на практике модельно-ориентированного подхода. Установлено, что наименее обеспеченными модельными, алгоритмическими и программными решениями являются вопросы, связанные с разработкой полного и корректного набора требований, а также с формализацией и верификацией технических проектов СПТС. Предложены способы решения существующих проблем посредством формирования единой модельно-языковой и информационно-программной среды разработки и верификации формальных моделей требований и архитектуры СПТС, построенных на основе оптимального набора взаимосвязанных fUML диаграмм, представленных в нотации языка ALF и верифицируемых в среде виртуальной машины fUML и с помощью SAT/SMT решателей.

1. Федеральный закон «О безопасности критической информационной инфраструктуры Российской Федерации». 12.07.2017 г.

2. Systems Engineering and Software Engineering https://www.sebokwiki.org/wiki/Systems_Engineering_and_Software_Engineering. (дата обращения 25.07.2018).

3. Laura E. Hart. Introduction to Model-Based System Engineering (MBSE) and SysML https://www.incose.org/docs/default-source/delaware-valley/mbse-overview-incose-30-july-2015.pdf. (дата обращения 21.06.2018).

4. The Standish Group Report CHAOS. https://www.projectsmart.co.uk/white-papers/chaos-report.pdf. (дата обращения 25.08.2018).

5. Dragan Milicev. Model-Driven Development with Ex ecutable UML. John Wiley & Sons, 2009, 720 p.

6. Sanford Friedenthal, Alan Moore, Rick Steiner. A Practical Guide to SysML: The Systems Modeling Language. Morgan Kaufmann, 3 edition, 2014, 630 p.

7. Lenny Delligatti. SysML Distilled: A Brief Guide to the Systems Modeling Language. Addison-Wesley Professional, 2013, 304 p.

8. Ковалёв С.П. Теоретико-категорный подход к метапрограммированию. М., ИПУ РАН, 2014, 112 стр.

9. Ковалeв С. П. Теоретико-категорный подход к проектированию программных систем. Фундаментальная и прикладная. математика, том 19, вып. 3, 2014, стр. 111–170.

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

11. Д.В. Буздалов, С.В. Зеленов, Е.В. Корныхин, А.К. Петренко, А.В. Страх, А.А. Угненко, А.В. Хорошилов. Инструментальные средства проектирования систем интегрированной модульной авионики. Труды ИСП РАН, том 26, вып. 1, 2014, стр. 201-230. DOI: 10.15514/ISPRAS-2014-26(1)-6

12. Зеленов С.В., Зеленова С.А. Моделирование программно-аппаратных систем и анализ их безопасности. Труды ИСП РАН, том 29, вып. 5, 2017 г., стр. 257-282. DOI: 10.15514/ISPRAS-2017-29(5)-13

13. http://www.ispras.ru/technologies/unitesk (дата обращения 17.10.2018)

14. Марков А.В. Автоматизация проектирования и анализа программного обеспечения с использованием языка UML и сетей Петри. Канд. дис., Новосибирск, НГТУ, 2015.

15. Saswat Anand et al. An Orchestrated Survey on Automated Software Test Case Generation. Journal of Systems and Software, vol. 86, Issue 8, 2013, pp. 1978-2001.

16. Yachai Limpiyakorn, Photchana Sawprakhon. Sequence Diagram Generation with Model Transformation Technology. In Proc. of the International MultiConference of Engineers and Computer Scientists, IMECS 2014, vol I,

17. Liping Li, Honghao Gao, Tang Shan. An Executable Model and Testing for Web Software based on Live Sequence Charts. In Proc. of the 2016 IEEE/ACIS 15th International Conference on Computer and Information Science (ICIS).

18. Thomas Buchmann and Alexander Rimer. Unifying Modeling and Programming with ALF. The Second International Conference on Advances and Trends in Software Engineering, vol I, IARIA, 2016. pp .10-15.

19. Shuhao Li, Sandie Balaguer 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

20. Felix Kurth. Automated Generation of Unit Tests from UML Activity Diagrams using the AMPL Interface for Constraint Solvers. Master Thesis, Hamburg University of Technology (TUHH), 2014.

21. Messaoud Rahim, Malika Boukala-Ioualalen, Ahmed Hammad. Petri Nets Based Approach for Modular Verification of SysML Requirements on Activity Diagrams. PNSE'14, a satellite event of Petri Nets 2014 and ACSD 2014, Tunis, Tunisia, pp 233-248.

22. Erwan Bousse, Tanja Mayerhofer, Benoit Combemale, Benoit Baudry. Advanced and efficient execution trace management for executable domain-specific modeling languages. Software & Systems Modeling, 2017, https://link.springer.com/article/10.1007/s10270-017-0598-5 (дата обращения 20.07.2018)

23. D. Savic, S. Vlajic, S. Lazarevic. Use Case specification using the SilabReq domain specific language. Computing and Informatics, vol. 34, 2015, 877–910.

24. Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig. 2018. Program Synthesis using Conflict-Driven Learning. In Proc. of 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM, New York, NY, USA, 16 p.

25. Ефремов Д.В, Мандрыкин М.У. Формальная верификация библиотечных функций ядра Linux. Труды ИСП РАН, том 29, вып. 6, 2017 г., стр. 49-76. DOI: 10.15514/ISPRAS-2017-29(6)-3