SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability

TL;DR

This paper presents a formal verification method using SMT-based techniques for LTL specifications with integer constraints, enabling faster runtime checking of service substitutability, especially for conversational services with data dependencies.

Contribution

It introduces an extension of Linear Temporal Logic with integer constraints and demonstrates its application to improve runtime verification of service substitutability.

Findings

Faster verification with smaller memory footprint.

Effective for conversational services with data dependencies.

Applicable to runtime checking in service-based applications.

Abstract

An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a different interface, for example if the former is no longer available. Standard Bounded Model Checking techniques can be used to perform this check, but they must be able to provide answers very quickly, lest the check hampers the operativeness of the application, instead of aiding it. The problem becomes even more complex when conversational services are considered, i.e., services that expose operations that have Input/Output data dependencies among them. In this paper we introduce a formal verification technique for an extension of Linear Temporal Logic that allows users to include in formulae constraints on integer variables. This technique applied to the substitutability problem for conversational services is shown to be considerably faster and with smaller memory footprint than existing ones.