Representation of the program model using predicates

Serhii Holub, Volodymyr Salapatov, Vadym Nemchenko

Abstract


The object of research in this article is the process of modeling programs and their subsequent development. The purpose of this article is to develop a methodology for describing and building software models in the form of nondeterministic finite automat. To achieve this goal, a task was set to improve the method for describing such models using predicates based on the MODEL CHECKING technology. The result of this article is a method for describing and presenting program models directly according to the chosen algorithm using predicates. If the program algorithm is chosen and described correctly, the resulting model should also be correct. The model will be a non-deterministic state machine that will not require further checking, as provided by the MODEL CHECKING technology. Structurally, the model will represent a special database, the processing of which will allow turning the model into a program in any procedural programming language. When developing parallel programs that are widely used for control in aviation, land transport, military affairs, etc., two additional states of the automaton are introduced into the model, which take into account the features of such programs. Therefore, a state monitor is provided for access to shared resources and a state protocol to process parallel branches of the program. To describe the algorithm of the program, we propose to present it in the form of a connected sequence of certain actions using predicates with the use of extended temporal logic. This description covers both the logic of the program and its branches and the specific actions at each location of the program model. With the help of this methodology, a program model of a stack algorithm was developed, which is the main component for the future automated system of processing the description of program models. The program which was created according to this technology, is currently in the testing and verification stage. The sequence of processing steps of such a model is shown in the example of a floating-point constant translation program. This program is also created using this technology in the target language assembly, has been fully tested, and has shown its functionality. This description covers both the logic of the program with its branches and the specific actions at each location of the application model. Conclusions: with a correct description of the program algorithm, an adequate model of it is built, with the help of which the program itself is created in the target procedural programming language. Note that in the conditions of the rapid development of management and control automation systems in various spheres of human activity, research on the creation of reliable based on the description of their models is an urgent problem.004.414.23:510.637

Keywords


model; predicate; temporal logic; an indeterminate finite automaton; procedural programming language

Full Text:

PDF

References


Hoare, C. A. R. Communicating sequential processes. Prentice Hall International Publ., 2022. 260 p. Available at: http://www.usingcsp.com/cspbook.pdf. (accessed 02.05.2023).

Milner, R. A Calculus of Communicating Systems. Book series: Lecture Notes in Computer Science. Springer Berlin, Heidelberg, 1980, vol. 92, 174 p. DOI: 10.1007/3-540-10235-3. Available at: http://www.lfcs.inf.ed.ac.uk/reports/86/ECS-LFCS-86-7/ECS-LFCS-86-7.pdf. (accessed 02.05.2023).

Clarke, E. M., Gramberg, O., Kroening, D., Peled, D. & Veith, H. Model Checking. Second edition. MIT Press Publ., 2018. 424 p. ISBN 0262349450. Available at: https://books.google.com.ua/books?id=qJl8DwAAQBAJ. (accessed 02.05.2023).

Zhang, Y. Ji, P.-F., Zhu, P.-W., Peng, P., Li, H.-W. & Jiang, J.-H. Parallel Software-Based Self-Testing with Bounded Model Checking for Kilo-Core Networks-on-Chip. Journal of Computer Science and Technology, 2014, vol. 38, pp. 405-421. DOI: 10.1007/s11390-022-2553-3.

Grobelna, I., Grobelny, M. & Adamski, M. Model checking of UML activity diagrams in logic controllers design. Advances in Intelligent Systems and Computing, 2014, vol. 286, pp. 233–242. DOI: 10.1007/978-3-319-07013-1_22.

Oshibka v PO Airbus A350 vynuzhdayet perezagruzhat' sistemy samoletov kazhdyye 149 chasov [Airbus A350 software bug forces aircraft systems to reboot every 149 hours]. Available at: https://internetua.com/oshibka-v-po-airbus-a350-vynujdaet-perezagrujat-sistemy-samoletov-kajdye-149-csasov. (accessed 02.05.2023). (in Russian).

Salapatov, V. I. Poryadok opysu i obrobky hrafa avtomatnoyi modeli [Order of the description and processing of the program automaton model graph]. Matematychni mashyny i systemy – Mathematical Machines and Systems, 2021, no 3, pp. 121-125. DOI: 10.34121/1028-9763-2021-3-121-125. (in Ukrainian).

Rumbaugh, J., Jakobson, I. & Booch, G. The Unified Modeling Language Reference Manual. Addison Wesley Longman, 1999, 568 p. ISBN 0-201-30998-X. Available at: https://idsi.md/files/file/referinte_utile_studenti/The%20Unified%20Modeling%20Language%20Reference%20Manual.pdf. (accessed 02.05.2023).

Lafore, R. Ob"yektno-oriyentirovannoye programmirovaniye v S++ [Object-oriented programming in C++]. SPb, Piter Publ., 2004. 928 p. (in Russian).

Eliens, A. Printsipy Obʺyektno-oriyentiro¬vannoy razrabotki programm. 2-ye izdaniye [Principles of Object-Oriented Software Development Second Edition]. Sankt-Peterburg, Vil'yams Publ., 2002. 496 p. ISBN 5-8459-0233-9. (in Russian).

Omelʹchenko, L. N. & Shevyakova, D. A. Samouchitel' Visual FoxPro 9.0 [Visual FoxPro 9.0 tutorial]. Sankt-Peterburg, BKHV-Peterburg Publ., 2005. 608 p. (in Russian).

Pasichnyk, V. V. & Reznychenko, V. A. Orha¬nizatsiya baz danykh ta znanʹ [Organization of databases and knowledge]. Kyiv, BHV Publ., 2006. 384 p. Available at: https://www.twirpx.com/file/1174516/. (accessed 02.05.2023). (in Ukrainian).

Garsia-Molina, H., Ullman, J. D. & Widom, J. Database System Implementation. United States Ed Edition, Prentice Hall, 1999. 653 p. ISBN-13: 978-0130402646.

Hopсroft, D. E., Motwani, R. & Ullman, J. D. Introduction to Automata Theory, Languages and Computation. 3rd Edition. Pearson Education Publ., 2006. 535 p. Available at: https://e.famnit.upr.si/pluginfile.php/636821/mod_page/content/8/Automata.pdf. (accessed 02.05.2023).

Konversʹkyy, A. Ye. Lohika (tradytsiyna i suchasna). Pidruchnyk dlya studentiv vyshchykh navchalʹnykh zakladiv [Logic (traditional and modern). The textbook for university students]. Kyiv, Tsentr uchbovoyi literatury Publ., 2008. 536 p. ISBN 978-966-364-735-7. (in Ukrainian).




DOI: https://doi.org/10.32620/reks.2024.1.01

Refbacks

  • There are currently no refbacks.