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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    From formal specifications to efficient test scenarios generation


    Beteiligte:
    Yang, Jing (Autor:in) / Ghazel, Mohamed (Autor:in) / El-Koursi, El-Miloudi (Autor:in)


    Erscheinungsdatum :

    01.05.2013


    Format / Umfang :

    1074780 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch





    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

    Hartrum, T.C. / Karagias, T. | IEEE | 1997