Modelling and Verifying an Object-Oriented Concurrency Model in GROOVE

TL;DR

This paper introduces an automatic method for verifying SCOOP concurrent programs by translating them into graph models and using GROOVE for simulation and verification of properties like deadlock freedom.

Contribution

It presents a novel graph transformation semantics for SCOOP and a translation tool that enables direct verification without source code modifications.

Findings

Successfully verified several SCOOP programs for deadlocks and correctness

Demonstrated the approach's effectiveness through case studies

Provided a fully automatic verification pipeline for SCOOP programs

Abstract

SCOOP is a programming model and language that allows concurrent programming at a high level of abstraction. Several approaches to verifying SCOOP programs have been proposed in the past, but none of them operate directly on the source code without modifications or annotations. We propose a fully automatic approach to verifying (a subset of) SCOOP programs by translation to graph-based models. First, we present a graph transformation based semantics for SCOOP. We present an implementation of the model in the state-of-the-art model checker GROOVE, which can be used to simulate programs and verify concurrency and consistency properties, such as the impossibility of deadlocks occurring or the absence of postcondition violations. Second, we present a translation tool that operates on SCOOP program code and generates input for the model. We evaluate our approach by inspecting a number of programs in the form of case studies.