Hardware-software codesign results of concurrent embedded real-time
systems are often not easily verifiable. The main difficulty
lies in the different time-scales of the embedded hardware, of the
embedded software, and of the environment. This rate difference
causes state-space explosions and hence coverification has been
mostly restricted to the initial system specifications. Currently,
most codesign tools or methodologies only support validation in
the form of cosimulation and testing. Here, we propose a new formal
coverification method based on linear hybrid automata. The
basic problems found in most coverification tasks are presented and
solved. For complex systems, a simplification strategy is proposed
to attack state-space explosions in formal coverification. Experimental
results show the feasibility of our approach and the increase
in verification scalability through the application of the proposed
method.
