Search academic texts

Information × Registration Number 0216U003108, 0113U000071 , R & D reports Title To develop algorithms for verification of structured systems with mobile agents. popup.stage_title Head Letichevsky Aleksander Adol'fovich, Registration Date 14-01-2016 Organization V.M.Glushkov Institute of Cubernetics of NASU popup.description2 3. Based on insertion models for the specification of multilevel protocols and programs, a system oriented towards the verification of applied transition systems is developed. This system combines fundamental developments on the analysis of programs with requirements of actual engineering practice of software design. The source language LiveUCM of the IMS system is developed on the basis of the graphic language UCM, which is widespread and accepted as an international standard, in which atomic actions, namely, the so-called obligations are concretized within the framework of this research. As such an action, it is proposed to use a local description, which is a basic concept of insertion models. This made it possible to apply a symbolic modeling complex to the analysis of systems specified in the LiveUCM language. The IMS system provides a complex solution to problems of symbolic transformation of logical formulas representing classes of states of an applied system and optimized verification of the satisfiability of these formulas. Solutions to the problem of verification of attainability in the space of such formulas are also proposed and include the development of the structure of the space of symbolic states and implementation of optimal search strategies and algorithms of abstraction of symbolic states, which provide the semi-decidability of procedures. With a view to simplifying algorithms for the proof of the satisfiability of formulas during the verification of systems, models of multicomponent systems are investigated in which only enumerated data types are used. In the environment of the IMS system, a knowledge base on system transitions with attributes of enumerated types is developed and implemented. With a view to simplifying algorithms for the proof of the satisfiability of formulas during the verification of systems, models of multicomponent systems are investigated in which only enumerated data types are used. In the environment of the IMS system, a knowledge base on system transitions with attributes of enumerated types is developed and implemented. The main application domains and directions on which the proposed methods and software tools are focused and in which they are successfully used are telecommunication, telematics, and the preparation of qualified specialists in the field of programming. The prognostic proposition for the further development of the objects of study is as follows: provide the enhancement of the proposed methodology and support tools - from program verification to program testing. Product Description popup.authors Волков Владислав Анатолійович Годлевський Олександр Богуславович Гребнєв Валерій Олександрович Губа Антон Андрійович Довбиш Валентина Яківна Колчин Олександр Валентинович Летичевський Олександр Адольфович Летичевський Олександр Олександрович Ляскало Леся Євгеніївна Матвєєва Людмила Євгенівна popup.nrat_date 2020-04-02 Close