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

Public Deposited
Resource Type
  • 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.

Thesis Degree Level
Thesis Degree Name
Thesis Degree Discipline
Rights Notes
  • Copyright © 2013 the author(s). Theses may be used for non-commercial research, educational, or related academic purposes only. Such uses include personal study, research, scholarship, and teaching. Theses may only be shared by linking to Carleton University Institutional Repository and no part may be used without proper attribution to the author. No part may be used for commercial purposes directly or indirectly via a for-profit platform; no adaptation or derivative works are permitted without consent from the copyright owner.
Date Created
  • 2013


In Collection: