Dynamic Actualization of Formal Model for Microcontrollers Software

The article proposes a method for dynamically updating a formal model of the process for debugging and verifying microcontroller software. The method is based on process mining technology and allows to record the observed behavior of the system in the form of a formal model, updating the process model in real time. This saves memory resources, preserves the cause-and-effect relationship between events, and allows to monitor systems with limited access. The effectiveness of the proposed method is demonstrated on a development board based on the STM32F103C8T microcontroller. The method is applicable for systems with memory of tens of KB and operating at a frequency of several MHz. The method is implemented as a library in C languages. A comparison is made with an approach based on the accumulation and post-processing of an event log. The time to add an event to the system, the time to update the model, and the amount of memory required to store information about the behavior of the system were estimated. Method allows to obtain models of processes in embedded systems in real time on limited resources, carry out software verification, determine the reachability of individual system states, and determine the causes of failures.