Various formal testing methods have been developed in the past decades. Most of them are based on graphical notations such as finite state machines, labelled transitions systems, etc., which remain quite intuitive for users to perform black box testing. In addition, testing methods based on temporal logics have been also investigated, such as the testing methods inspired by model checking. However, testing with model checkers often needs a model of System Under Test (SUT) to be known. This paper discusses a method for generating test cases from specifications expressed in CTL∗ temporal logic, under a black-box framework. The test generation process from CTL∗ is inspired by Banerjee et al.'s work [1] which has developed a technique to generate non-vacuous test scenarios from LTL properties. The essential step of our test generation method is to rewrite a pertinent CTL∗ property in terms of present state Boolean propositions and X(Next)-guarded temporal properties. The generated test benches are implemented within the ControlBuild tool.
From formal specifications to efficient test scenarios generation
2013-05-01
1074780 byte
Conference paper
Electronic Resource
English
SYNTHESIZING TRAFFIC SCENARIOS FROM FORMAL SPECIFICATIONS FOR TESTING AUTOMATED VEHICLES
British Library Conference Proceedings | 2020
|Test case generation from formal specifications on the example of train control systems
British Library Conference Proceedings | 2000
|Generation of Object-Oriented Formal Software Specifications
British Library Conference Proceedings | 1997
|AUTOMATED AIRCRAFT INTENT GENERATION PROCESS BASED ON SPECIFICATIONS EXPRESSED IN FORMAL LANGUAGES
European Patent Office | 2017
|