Embedded software verification in hardware-software codesign

Concurrent Embedded Real-Time Software (CERTS) is intrinsically different f rom traditional, sequential, independent, and temporally unconstrained soft ware. The verification of software is more complex than hardware due to inh erent flexibilities (dynamic behavior) that incur a multitude of possible s ystem states. The verification of CERTS is all the more difficult due to it s concurrency and embeddedness. The work presented here shows how the compl exity of CERTS verification can be reduced significantly through answering common engineering questions such as when, where, and how one must verify e mbedded software. First, a new Schedule-Verify-Map strategy is proposed to answer the when question. Second, verification under system concurrency is proposed to answer the where question. Finally, a complete symbolic model c hecking procedure is proposed for CERTS verification. Several application e xamples illustrate the usefulness of our technique in increasing verificati on scalability. (C) 2000 Elsevier Science B.V. All rights reserved.