We present a method for automatically generating test sequences to satisfy MC/DC like structural coverage criteria of software behavioral models specified in state-based formalisms. The use of temporal logic for characterizing test criteria and the application of model-checking techniques for generating test sequences to those criteria have been of interest in software verification research for some time. Nevertheless, criteria for which constraints span more than one test sequence, such as the modified condition/decision coverage (MC/DC) mandated for critical avionics software, cannot be characterized in terms of a single temporal property. This paper discusses a method for recasting two-sequence constraints in the original model as a single sequence constraint expressed in temporal logic on a slightly modified model. The test-sequence generated by a model-checker for the modified model can be easily separated into two different test-sequences for the original model, satisfying the given test criteria. The approach has been successful in generating MC/DC test sequences from a model of the mode-logic in a flight-guidance system.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Generating MC/DC adequate test sequences through model checking


    Beteiligte:
    Rayadurgam, S. (Autor:in) / Heimdahl, M.P.E. (Autor:in)


    Erscheinungsdatum :

    2004


    Format / Umfang :

    6 Seiten, 15 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    System safety property-oriented test sequences generating method based on model checking

    Zhang, Y. / Zhao, X.Q. / Zheng, W. et al. | British Library Conference Proceedings | 2010


    METHOD FOR AUTOMATICALLY GENERATING ADEQUATE ROUTE DATA

    OLIVER RUOFF / DANIELE MAURO / SIMON GEISLER | Europäisches Patentamt | 2023

    Freier Zugriff