Concurrent Embedded Real-Time Software (CERTS) is intrinsically
different from traditional, sequential, independent, and temporally
unconstrained software. The verification of software is more
complex than hardware due to inherent flexibilities (dynamic behavior)
that incur a multitude of possible system states. The verification of
CERTS is all the more difficult due to its concurrency and
embeddedness. The work presented here shows how the complexity of
CERTS verification can be reduced significantly through answering
common engineering questions such as when, where, and
how one must verify embedded 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 checking procedure is proposed
for CERTS verification.
Several application examples illustrate the usefulness of our technique in
increasing verification scalability.