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, we propose a new formal
coverification approach 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 our approach and the increase in verification
scalability through the application of the proposed method.