Zakutaylo D. The corrective design of the hardware and software package of computer systems on the basis of logical languages of specifications and modern languages of description of discrete systems

The scientific novelty of the obtained results consists in the following: there were developed temporal logics LCTL (Local Computational Tree Logic) and GCTL (Global Computational Tree Logic) that allow to describe in quantitative way the temporal properties of the verifying algorithms. Semantics of these temporal logics allow to use the model of the verifying algorithms with number of states which are less than that for the corresponding models for the existing temporal logics and their semantics; for the first time there were developed the new methods of the program translation from the VHDL language, which uses the constructs with temporal delays into transition system; the new methods are devised for proposed logics which will enable to verify properties with explicit real-time constraints, the new evaluation was obtained of the temporal complexity of the proposed method for the model-checking problem for LCTL logic.