Model Sketching by Abstraction Refinement for Lifted Model Checking (Extended Version)

TL;DR

This paper introduces a method for synthesizing complete Promela models from partial sketches by leveraging abstraction refinement techniques tailored for family-based model checking of software product lines.

Contribution

It presents a novel approach combining abstraction refinement with lifted model checking to synthesize models from sketches in the context of software product lines.

Findings

Effective synthesis of models from sketches demonstrated

Improved verification efficiency for model families

Applicable to software product line analysis

Abstract

In this work, we show how the use of verification and analysis techniques for model families (software product lines) with numerical features provides an interesting technique to synthesize complete models from sketches (i.e.\ partial models with holes). In particular, we present an approach for synthesizing Promela model sketches using variability-specific abstraction refinement for lifted (family-based) model checking.