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.
[download the pdf file] [url]