A test selection language for CO-OPN specifications

In this paper we propose a test language that allows expressing test intentions for CO-OPN (concurrent object-oriented Petri nets) specifications - a formal specification language designed to handle large complex concurrent systems. Our test language is based on temporal logic formulas for expressing graphs of input/output pairs - the inputs correspond to operations performed on the system and the outputs to the observable results of those operations. We encapsulate the temporal logic using a language of constraints, which purpose is to shape the tests that are to be produced. In this paper we discuss the syntax and provide the semantics of this test language. One of our main worries while designing the test language were to keep it modular in order to promote reusability. Another worry was to be able to cope with non-determinism coming from the system under test. We illustrate managing non-determinism as well as other features of our language by showing how we can generate tests for the login part of an e-banking system. A framework for editing CO-OPN specifications exists and one of its features is the possibility of automatically generating high level Java prototypes that can be completed/extended by human developers. We discuss the applicability and the usefulness of our test language while verifying systems built using this methodology.