Verifying Real-Time Embedded Software by Means of Automated State-based Online Testing and the SPIN Model Checker—Application to RTEdge Models

Verifying a real time embedded application is very challenging especially since one has to consider timing requirements in addition to functional ones. Through online testing, the risks of failure in real time applications are reduced. During online state-based testing the generation and execution of test cases happens concurrently: test case generation uses information from a state-based test model in combination with observed execution behaviour. This thesis describes a practical online testing algorithm that is implemented in the state-based modeling tool RTEdge developed at Edgewater Computer Systems Inc. In addition, thanks to RTEdge’s mechanism to map the state model to Promela, thereby allowing the use of the SPIN model checker, when additional coverage is needed after the online testing procedure, SPIN is used to generate additional test cases that will increase coverage. The case studies show that our online testing algorithm produces a test suite that achieves high model coverage.