Order of the description and processing of the program automaton model graph

Abstract

The article considers the method for describing program modeling where predicates are used to create a model in the form of a nondeterministic finite automaton. A format of the description of predicates with the division of their semantic and conditional parts is offered in the paper. Arithmetic operators, parentheses, standard functions, as well as temporal logic operators U and N should be used to describe the content of the predicate. For the logical part of predicates, in addition to their logical functions, it is proposed to use relation operations, arithmetic operators, parentheses and standard functions. The formation of the description of each state of the program automaton model should be completed by dividing into different branches of the model. To describe the models of parallel programs, the following special states have been introduced: a state-monitor for the access of various processes to shared resources and a state-protocol for the description of independent parallel branches. The model is created in the process of its description, so it does not require further verification. If the description of the model is performed correctly and the optimal algorithm of the future program is selected, such model will fully correspond to its description. Unlike MODEL CHECKING technology, which requires verification, it eliminates the need for model verification. The graph of the obtained model is processed by its sequential traversal on all branches with returns to the previous states and subsequent software implementation. Consecutive traversing should be performed for each branch of the model either to its final state or to the state that has already been processed during the traversal. Model processing includes transmission of the model description into an internal representation for subsequent conversion into a program in the target procedural programming language. In this case all actions in the substantive parts of the predicates, as well as the conditions of the branches in the process of transmission are converted into an internal representation of the program. This technology provides a direct conversion of the description of the program model into the program itself.