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 c onsequences when high-assurance systems are codesigned. The main difficulty lies in the different time-scales of the embedded hardware, of the embedde d 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. Curren tly, most codesign tools or methodologies only support validation in the fo rm of cosimulation and testing of design alternatives. Here, a new formal c overification approach is proposed based on linear hybrid automata. The bas ic timing problems found in most coverification tasks are presented and sol ved. For complex systems, a simplification strategy is proposed to attack t he state-space explosion occurring in formal coverification. Experimental r esults show the feasibility of the approach and the increase in verificatio n scalability through the application of the proposed method.