Concurrent Embedded Real-Time Software Verification
Abstract
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 "Concurrent Embedded
Real-Time Software" (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. Application examples
illustrate the usefulness of our technique in increasing
verification scalability.
Keywords: Embedded Software, Software Verification,
Symbolic Model Checking, System/Process Concurrency,
Quasi-static Scheduling, Software Synthesis