Hardware-software 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 hard,rare, of the embedded software, and of the environment. This difference makes hardware-software coverification nor 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, Me propose a new formal coverification method based on linear hybrid automata The basic problems found in most coverification tasks are presented and soh ed. 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.