On Formal Description of Microcontroller and Program Interoperability: Deriving FSM Composition

In this paper, approaches to the formal description of interactions between a microcontroller and a program are investigated. We consider the finite state machine (FSM) as a formal model of each component's behavior. The construction of FSM composition is well-studied for cases where the operating mode is synchronous or parallel. In practice, there are cases when a more complex (mixed) operating mode is needed. The interoperability of the microcontroller and the program is very similar to the parallel mode; however, there may be situations where the microcontroller must simultaneously emit a signal to the external environment and the program. Therefore, the parallel composition operation cannot be used to describe the functioning of the hardware-software complex. Thus, it is necessary to define a new composition operation with multiple reactions of the external component to derive test suites for the whole system. An algorithm for constructing FSM composition with multiple reactions of an external component is suggested. It is shown that inserting an additional component (dividing the microcontroller into two components) does not allow substituting the composition with multiple reactions of an external component by iteratively deriving binary parallel compositions.