Hardware-software timing coverification of concurrent embedded real-time systems

The results of hardware-software codesign of concurrent embedded real-time systems are often not verified or not easily verifiable. This has serious consequences when high-assurance systems are codesigned. The main difficulty lies in the different time-scales of the embedded hardware, of the embedded software, and of the environment. This difference makes hardware-software timing coverification not only a difficult task for most systems, but has also restricted coverification to the initial system specifications. Currently, most codesign tools or methodologies only support validation in the form of cosimulation and testing of design alternatives. Here, a new formal coverification approach is proposed based on linear hybrid automata. The basic timing problems found in most coverification tasks are presented and solved. For complex systems, a simplification strategy is proposed to attack the state-space explosion occurring in formal coverification. Experimental results show the feasibility of the approach and the increase in verification scalability through the application of the proposed method.