Timing coverification of concurrent embedded real-time systems
Pao‐Ann Hsiung · 1999
Hardware-software codesign results of c~ncurrcnt embedded realtime systems are often not easily verifiable.The main difficulty lies in-the different time-scales df the embedded hardware, of thk embedded software, and of the environment.This rate difference cawes state-space explosions and hence coverification has been mostly restricted t0 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 automam.The basic problems found in nm~t coveritication tasks are presented and solved.For complex systems, a simplification strategy is proposed to attack state-space explosions in formal covedtication.Experimental results show the feasibility of our approach and the increase in verification scalability through the application of the proposed method.