Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar
Model checking of real-time systems has evolved throughout the years. Recently, the model checker Ecdar, using timed I/O automata, was used to perform compositional verification. However, in order to fully integrate model checking of real-time systems into industrial development, we need a productiv...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2018-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1809.03889v1 |
| _version_ | 1811277646931165184 |
|---|---|
| author | Tobias R. Gundersen Florian Lorber Ulrik Nyman Christian Ovesen |
| author_facet | Tobias R. Gundersen Florian Lorber Ulrik Nyman Christian Ovesen |
| author_sort | Tobias R. Gundersen |
| collection | DOAJ |
| description | Model checking of real-time systems has evolved throughout the years. Recently, the model checker Ecdar, using timed I/O automata, was used to perform compositional verification. However, in order to fully integrate model checking of real-time systems into industrial development, we need a productive and reliable way to test if such a system conforms to its corresponding model. Hence, we present an extension of Ecdar that integrates conformance testing into a new IDE that now features modelling, verification, and testing. The new tool uses model-based mutation testing, requiring only the model and the system under test, to locate faults and to prove the absence of certain types of faults. It supports testing using either real-time or simulated time. It parallelises test-case generation and test execution to provide a significant speed-up. We also introduce new mutation operators that improve the ability to detect and locate faults. Finally, we conduct a case study with 140 faulty systems, where Ecdar detects all faults. |
| first_indexed | 2024-04-13T00:20:38Z |
| format | Article |
| id | doaj.art-c629997cb8a4465e9374eacff7276377 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T00:20:38Z |
| publishDate | 2018-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-c629997cb8a4465e9374eacff72763772022-12-22T03:10:48ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-09-01277Proc. GandALF 201814716010.4204/EPTCS.277.11:10Effortless Fault Localisation: Conformance Testing of Real-Time Systems in EcdarTobias R. Gundersen0Florian Lorber1Ulrik Nyman2Christian Ovesen3 Aalborg University Aalborg University Aalborg University Aalborg University Model checking of real-time systems has evolved throughout the years. Recently, the model checker Ecdar, using timed I/O automata, was used to perform compositional verification. However, in order to fully integrate model checking of real-time systems into industrial development, we need a productive and reliable way to test if such a system conforms to its corresponding model. Hence, we present an extension of Ecdar that integrates conformance testing into a new IDE that now features modelling, verification, and testing. The new tool uses model-based mutation testing, requiring only the model and the system under test, to locate faults and to prove the absence of certain types of faults. It supports testing using either real-time or simulated time. It parallelises test-case generation and test execution to provide a significant speed-up. We also introduce new mutation operators that improve the ability to detect and locate faults. Finally, we conduct a case study with 140 faulty systems, where Ecdar detects all faults.http://arxiv.org/pdf/1809.03889v1 |
| spellingShingle | Tobias R. Gundersen Florian Lorber Ulrik Nyman Christian Ovesen Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar Electronic Proceedings in Theoretical Computer Science |
| title | Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar |
| title_full | Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar |
| title_fullStr | Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar |
| title_full_unstemmed | Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar |
| title_short | Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar |
| title_sort | effortless fault localisation conformance testing of real time systems in ecdar |
| url | http://arxiv.org/pdf/1809.03889v1 |
| work_keys_str_mv | AT tobiasrgundersen effortlessfaultlocalisationconformancetestingofrealtimesystemsinecdar AT florianlorber effortlessfaultlocalisationconformancetestingofrealtimesystemsinecdar AT ulriknyman effortlessfaultlocalisationconformancetestingofrealtimesystemsinecdar AT christianovesen effortlessfaultlocalisationconformancetestingofrealtimesystemsinecdar |