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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    From formal specifications to efficient test scenarios generation


    Contributors:


    Publication date :

    2013-05-01


    Size :

    1074780 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English




    SYNTHESIZING TRAFFIC SCENARIOS FROM FORMAL SPECIFICATIONS FOR TESTING AUTOMATED VEHICLES

    Klischat, Moritz / Althoff, Matthias | British Library Conference Proceedings | 2020


    Test case generation from formal specifications on the example of train control systems

    zu Horste, M. M. / Schnieder, E. / Schulz, H.-M. et al. | British Library Conference Proceedings | 2000


    Generation of Object-Oriented Formal Software Specifications

    Karagias, T. / Hartrum, T. / IEEE | British Library Conference Proceedings | 1997


    AUTOMATED AIRCRAFT INTENT GENERATION PROCESS BASED ON SPECIFICATIONS EXPRESSED IN FORMAL LANGUAGES

    HARDT MICHAEL W / NAVARRO FELIX FRANCISCO A | European Patent Office | 2017

    Free access