Concurrent Embedded Real-Time Software Verification

Pao-Ann Hsiung
Institute of Information Science
Academia Sinica, Taipei, Taiwan.
( the 24th IEEE Computer Society International Computer Software and Applications Conference (COMPSAC'00) , October 2000, Taipei, Taiwan.)


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