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.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