In runtime verification, operational models describing the expected system behavior offer some advantages with respect to declarative specifications of properties, especially when designers are more accustomed to them. However, nondeterminism in the specification usually affects performances of those operational methods that explicitly represent all the possible conformant states. In this paper, we tackle the problem of dealing with nondeterminism in an operational runtime verification approach based on the use of Abstract State Machines (ASMs). We propose an SMT-based technique in which ASM computations are symbolically represented and conformance verification is performed by means of satisfability checking. Experiments show that, in most of the cases, the symbolic approach performs better than a technique for ASM-based runtime verification explicitly representing the conformant states.

(2014). Using SMT for dealing with nondeterminism in ASM-based runtime verification [conference presentation - intervento a convegno]. In ELECTRONIC COMMUNICATIONS OF THE EASST. Retrieved from http://hdl.handle.net/10446/31429

Using SMT for dealing with nondeterminism in ASM-based runtime verification

ARCAINI, Paolo;GARGANTINI, Angelo Michele;
2014-01-01

Abstract

In runtime verification, operational models describing the expected system behavior offer some advantages with respect to declarative specifications of properties, especially when designers are more accustomed to them. However, nondeterminism in the specification usually affects performances of those operational methods that explicitly represent all the possible conformant states. In this paper, we tackle the problem of dealing with nondeterminism in an operational runtime verification approach based on the use of Abstract State Machines (ASMs). We propose an SMT-based technique in which ASM computations are symbolically represented and conformance verification is performed by means of satisfability checking. Experiments show that, in most of the cases, the symbolic approach performs better than a technique for ASM-based runtime verification explicitly representing the conformant states.
2014
Arcaini, Paolo; Gargantini, Angelo Michele; Riccobene, Elvinia
File allegato/i alla scheda:
File Dimensione del file Formato  
avocs2014_postProceedings.pdf

Solo gestori di archivio

Descrizione: author's postprint - versione referata
Dimensione del file 358.63 kB
Formato Adobe PDF
358.63 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/31429
Citazioni
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact