Testing Real-Time Systems Using UPPAAL
This chapter presents principles and techniques for model-based black-box conformance testing of real-time systems using the Uppaal model-checking tool-suite. The basis for testing is given as a network of concurrent timed automata specified by the test e
- PDF / 1,060,384 Bytes
- 41 Pages / 430 x 660 pts Page_size
- 94 Downloads / 158 Views
2
Department of Information Technology, Uppsala University, P.O. Box 337, SE-751 05 Uppsala, Sweden {hessel,paupet}@it.uu.se Department of Computer Science, Aalborg University, Fredrik Bajersvej 7E, DK-9220 Aalborg, Denmark {kgl,marius,bnielsen,ask}@cs.aau.dk Abstract. This chapter presents principles and techniques for modelbased black-box conformance testing of real-time systems using the Uppaal model-checking tool-suite. The basis for testing is given as a network of concurrent timed automata specified by the test engineer. Relativized input/output conformance serves as the notion of implementation correctness, essentially timed trace inclusion taking environment assumptions into account. Test cases can be generated offline and later executed, or they can be generated and executed online. For both approaches this chapter discusses how to specify test objectives, derive test sequences, apply these to the system under test, and assign a verdict.
1
Introduction
Many computer-based systems monitor and control a physical environment through sensors and actuators. The physical laws governing the environment induce a set of real-time constraints which the system must obey in order to achieve satisfactory or safe operation. Thus the computer system must not only produce correct result or reaction, but must do so at the correct time; neither too early nor too late. For a real-time system the timely reaction is just as important as the kind of reaction. Testing real-time systems is even more challenging than testing untimed reactive systems, because the tester must now consider when to stimulate system, when to expect responses, and how to assign verdicts to the observed timed event sequence. Further, the test cases must be executed in real-time, i.e., the test execution system itself becomes a real-time system. In this chapter we introduce a formal approach to model-based black-box conformance testing of real-time systems. We aim both at introducing timed testing to readers that are new in the area by giving many examples, and to more experienced readers by being formally precise and by touching on more advanced topics. 1.1
Approach and Chapter Outline
Real-time influences all aspects of test generation: The specification language must allow for the specification of real-time constraints. The conformance R.M. Hierons et al. (Eds.): Formal Methods and Testing, LNCS 4949, pp. 77–117, 2008. c Springer-Verlag Berlin Heidelberg 2008
78
A. Hessel et al.
(implementation) relation must define what real-time behavior should be considered correct. It should be possible to specify what parts of the specified behavior should be tested. This can be done through test purposes, coverage criteria, or random exploration. Finally, the test generation algorithm must analyze the real-time specification, select and instantiate test cases, and output these in a timed test notation language. This computation must be done efficiently in order to handle large and complex specifications. The timed automata formalism has become a popular and wides
Data Loading...
