Formal verification of coupling properties for an automotive software integration across XIL

Virtualization and desktop testing of an integrated system without inclusion of a physical hardware is a well-established concept due to today's abundant computing power availability. However, only few aspects of reality are introduced in steps into these virtual environments. The aspects of reality like hard-real time deadlines, timing events, coupling frequency and data synchronization between two subsystems in a system offer complexity without fair estimation of its consequence on the system behavior. In this paper, we describe the abovementioned complexity as the coupling properties detailed for a combustion engine example along with its controller. We formally verify the timing, safety, liveness and deadlock properties of the coupling by modeling them as timed transition systems. The example is verified for the idle speed control, smooth mode switching and for injection cutoff control where the interaction between the subsystems is very critical. The paper highlights a very important perspective of strong and weak subsystem coupling while transiting from Model-in-the-loop (MiL) to Software-in-the-Loop (SiL) and finally to Hardware-in-the-Loop (HiL). In conclusion, the input-output behavior of the coupled subsystems is also presented for a realistic observation of the control loop.