Preview

Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS)

Advanced search

Methodology and Tools for Development and Verification of formal fUML Models of Requirements and Architecture for Complex Software and Hardware Systems

https://doi.org/10.15514/ISPRAS-2018-30(5)-8

Abstract

The article presents models and algorithms to support end-to-end quality control of complex software and hardware systems through the implementation of the software-controlled process of development and verification of formal models of requirements and architecture of such systems, Firstly, we give the analysis of scientific publications and the normative-methodical base in the field of development and application in practice of the model-based approach is given. We establish that least provided by model, algorithmic and software solutions are issues related to the development of a complete and correct set of requirements, as well as the formalization and verification of technical projects of software and hardware systems. To solve the existing problems, we propose to develop a special unified environment for the development, modeling and testing formal models of requirements and architecture of complex software and hardware systems. These models provide an optimal set of interconnected fUML diagrams presented in ALF notation and verified in the fUML virtual machine and using SMT/SAT solvers.

About the Authors

A. V. Samonov
Mozhaiskiy Military Space Academy
Russian Federation


G. N. Samonova
Mozhaiskiy Military Space Academy
Russian Federation


References

1. Federal law "On security of critical information infrastructure of the Russian Federation". 12.07.2017 (in Russian)

2. Systems Engineering and Software Engineering, https://www.sebokwiki.org/wiki/Systems_Engineering_and_Software_Engineering. (accessed 25.07.2018).

3. Laura. 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. (accessed 21.06.2018).

4. The Standish Group Report CHAOS. https://www.projectsmart.co.uk/white-papers/chaos-report.pdf. (accessed 25.08.2018).

5. Dragan Milicev. Model-Driven Development with Executable 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. Kovalev S.P. Theoretical and categorical approach to metaprogramming. M., IPU Russian Academy of Sciences, 2014, 112 p. (in Russian)

9. Kovalev S.P. Category-Theoretic Approach to Software Systems Design. Journal of Mathematical Sciences, vol. 214, issue 6, 2016, pp. 814-853.

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. D.V., Buzdalov, S.V. Zelenov, E.V. Kornykhin, A.K. Petrenko, V.A. Fear, A.A. Ognenko, A.V. Khoroshilov. Design tools for integrated modular avionics systems. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 201-230. DOI: 10.15514/ISPRAS-2014-26(1)-6 (in Russian)

12. S.V. Zelenov, S.A. Zelenova, Modeling of hardware and software systems and analyze their security. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 5, 2017, pp. 257-282. DOI: 10.15514/ISPRAS-2017-29(5)-13 (in Russian)

13. http://www.ispras.ru/technologies/unitesk (accessed 17.10.2018) (in Russian)

14. Markov, A.V., automation of design and analysis software using UML and Petri nets. PhD Thesis, NSTU, Novosibirsk, 2015 (in Russian).

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 (accessed 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.b of 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM, New York, NY, USA, 16 p.

25. Efremov D. V., Mandrykin M. U. Formal verification of Linux kernel library functions. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 6, 2017, pp. 49-76. DOI: 10.15514/ISPRAS-2017-29(6)-3 (in Russian)


Review

For citations:


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. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(5):123-146. (In Russ.) https://doi.org/10.15514/ISPRAS-2018-30(5)-8



Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.


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