A framework for the test and verification of real-time systems

As real-time computer systems become larger and more complex, so their analysis becomes increasingly difficult. Much of the skill in developing these systems lies in choosing the most appropriate theories and tools for different stages of development and different aspects of the system. But however rigorously a system is verified it is always necessary to test implementations in order to check that the behaviour of the real system has been correctly captured by the model. This paper addresses some problems of integrating testing with existing theories for the formal development of real-time systems. Our approach allows theories and tools for verification and testing to be combined in a principled manner. In this paper we describe our framework in terms of the formal link between test and verification and the relation of formal test models to implemented real-time systems. Finally, we suggest some ways of integrating test and verification in order to build efficient formal development methods