This utility model relates to an automatic validation of control systems and can be used in the development of control systems, microcontroller programming. The technical result of the proposed device is to expand the functionality of processes to identify errors in microcontroller systems to manage the program by providing a formal model checking control program designed to meet the specifications, which can be drawn in terms of temporal logic. The technical result is achieved in that the device for formal verification of consistency of the control program of microcontroller system given specification, including testing module units operative data storage control unit, checking of results processing unit, wherein the control unit with its first output connected to a block of operational data storage, and second access to the test results of the processing unit, the interface terminal block is connected with the control output of the control unit and information input to the unit of processing test results performed so that the test module is a module formal verification model matching evaluation unit associated with the block of operational data storage control unit is a microcontroller, data outputs interface distribution unit connected to the control unit through an input unit model and an input unit specification in the absence of permanent data storage unit, evaluation unit associated with the storage unit operative yes nnyh to give recommendations to the user in the form of procedures full formal model matching control program microcontroller system and a predetermined specification.
展开▼
