Show Me New Counterexamples: A Path-Based Approach
| Autor: | Virginie Wiels, Hélène Waeselynck, Kalou Cabrera Castillos |
|---|---|
| Přispěvatelé: | Équipe Tolérance aux fautes et Sûreté de Fonctionnement informatique (LAAS-TSF), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, ONERA - The French Aerospace Lab [Toulouse], ONERA, Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT) |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Model checking
Theoretical computer science Programming language Computer science Process (engineering) media_common.quotation_subject 020207 software engineering model-checking 02 engineering and technology computer.software_genre synchronous data-flow models Domain (software engineering) Data modeling Algorithmic program debugging Debugging TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Path (graph theory) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO]Computer Science [cs] structural analysis computer Counterexample media_common |
| Zdroj: | 8th IEEE International Conference on Software Testing, Verification, and Validation (ICST 2015) 8th IEEE International Conference on Software Testing, Verification, and Validation (ICST 2015), Apr 2015, Graz, Austria. ⟨10.1109/ICST.2015.7102606⟩ ICST |
| DOI: | 10.1109/ICST.2015.7102606⟩ |
| Popis: | International audience; We consider lightweight usage of model-checking for the debugging of Simulink models. A problem is that model-checkers typically return only one counterexample, which may slow down the debugging process. We propose an approach and a tool to produce several counterexamples, exemplifying different property violation patterns for a given version of the design. The approach uses data collected during the replay of the counterexamples to synthesize queries for the model-checker, so that it finds counterexamples that activate new paths. The approach is applied to an academic example and an industrial model from the automotive domain. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|