Temporal property patterns for model-based testing from UML/OCL

This article describes a new property- and model-based testing approach using UML/OCL models, driven by temporal property patterns and a tool for assisting the temporal properties formalization. The patterns are expressed in the TOCL language, an adaptation of Dwyer's property patterns to OCL. The patterns are used to formalize temporal requirements without having to learn a complex temporal logics such as LTL or CTL. From these properties, automata are automatically computed. These can be used for two purposes. First, it is possible to evaluate the quality of a test suite by measuring the coverage of a property using its associated automaton. Second, the automaton can be used to drive the test generation in order to produce complementary test cases. To this end, we defined dedicated coverage criteria, targeting specific events of the property, and aiming either at illustrating the expected behaviour of the system, or checking its robustness w.r.t. the property. However, it was observed that the semantics of the property language may be more subtle that it seems. To facilitate the adoption of the language by industrials, we have proposed a tool-supported assistant for property design, aiming to help the validation engineer choosing which constructs faithfully correspond to his intention. This approach has been experimented on several case studies with industrial partners. It has shown its interest for software validation, providing useful information thanks to adequate traceability features.