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

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.