nuXmv is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include MTL0,∞ formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing nuXmv with other verification tools for timed automata and MTL0,∞ , considering different benchmarks from the literature. The results show that nuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for MTL0,∞ .

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties / Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano. - 11561:(2019), pp. 376-386. (Intervento presentato al convegno International Conference on Computer Aided Verification, CAV 2019 tenutosi a New York City, NY, USA nel 15-18 July 2019) [10.1007/978-3-030-25540-4_21].

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties

Cimatti, Alessandro;Griggio, Alberto;Magnago, Enrico;Roveri, Marco;Tonetta, Stefano
2019-01-01

Abstract

nuXmv is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include MTL0,∞ formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing nuXmv with other verification tools for timed automata and MTL0,∞ , considering different benchmarks from the literature. The results show that nuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for MTL0,∞ .
2019
Proceedings of Computer Aided Verification - 31st International Conference, CAV 2019
USA
SPRINGER
978-3-030-25539-8
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano
Extending nuXmv with Timed Transition Systems and Timed Temporal Properties / Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano. - 11561:(2019), pp. 376-386. (Intervento presentato al convegno International Conference on Computer Aided Verification, CAV 2019 tenutosi a New York City, NY, USA nel 15-18 July 2019) [10.1007/978-3-030-25540-4_21].
File in questo prodotto:
File Dimensione Formato  
TimednuXmv.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Creative commons
Dimensione 345.42 kB
Formato Adobe PDF
345.42 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/258760
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 19
  • ???jsp.display-item.citation.isi??? 17
social impact