Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that (i) abstracts the initial (faulty) TA tainit in a PTA pta; (ii) generates some test data (i.e., timed traces) from pta; (iii) assesses the correct evaluation of the traces with the oracle; (iv) uses the IMITATOR tool for synthesizing some constraints φ on the parameters of pta; (v) instantiate from φ a TA tarep as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user.

(2019). Repairing Timed Automata Clock Guards through Abstraction and Testing . Retrieved from http://hdl.handle.net/10446/151144

Repairing Timed Automata Clock Guards through Abstraction and Testing

Arcaini, Paolo;Gargantini, Angelo;Radavelli, Marco
2019-01-01

Abstract

Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that (i) abstracts the initial (faulty) TA tainit in a PTA pta; (ii) generates some test data (i.e., timed traces) from pta; (iii) assesses the correct evaluation of the traces with the oracle; (iv) uses the IMITATOR tool for synthesizing some constraints φ on the parameters of pta; (v) instantiate from φ a TA tarep as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user.
2019
André, Étienne; Arcaini, Paolo; Gargantini, Angelo Michele; Radavelli, Marco
File allegato/i alla scheda:
File Dimensione del file Formato  
taRepairTAP2019.pdf

Solo gestori di archivio

Versione: postprint - versione referata/accettata senza referaggio
Licenza: Licenza default Aisberg
Dimensione del file 755.23 kB
Formato Adobe PDF
755.23 kB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/151144
Citazioni
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 8
social impact