Automatic test case generation with region-related coverage annotations for real-time systems

Testing is the mainstream of verification techniques used for real-time systems in the industry because it allows the engineers to directly observe how their system implementations react to various test cases. In this paper, we investigate how to use symbolic techniques to automatically generate test cases for real-time systems. Especially, our test cases have two annotations that can be useful in the construction of powerful test cases. First, events in our test cases are labeled with symbolic timing constraints which can either be conveniently used in picking event occurrence times or be used for choosing boundary timing values in domain analysis. Second, our test cases are annotated with regionrelated coverage estimations which support high precision in detecting some timing bugs. Finally, we have implemented our ideas with BDD-like data-structures which could lead to performance advantage for testing complex embedded systems.