Representation of the program model using predicates

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