Most of current codesign tools or methodologies only support validation in the
form of cosimulation and testing of design alternatives. The results of
hardware-software codesign of a distributed system are often not verified,
because they are not easily verifiable. In this paper, we propose a new formal
coverification approach based on linear hybrid automata, and an algorithm for
automatically converting codesign results to the linear hybrid automata
framework. Our coverification approach allows automatic verification of
real-time constraints such as hard deadlines. Another advantage is that
the proposed approach is suitable for verifying distributed systems with
arbitrary communication patterns and system architecture. The feasibility
of our approach is demonstrated through several application examples.
The proposed approach has also been successfully used in verifying deadline
violations when there are inter-task communications between tasks with
different period lengths.