| Abstrakt: |
We present a novel approach to synthesize complete models from Promelamodel sketches by using of lifted (family-based) verification and analysis techniques for model families (a.k.a software product lines—SPLs). The input is a Promelamodel sketch, which represents a partial model with missing numerical holes. The goal is to automatically synthesize values for the holes, such that the resulting complete model satisfies a given Linear Temporal Logic (LTL) specification. First, we encode a model sketch as a model family, such that all possible sketch realizations correspond to possible variants in the model family. Then, we preform a lifted (family-based) model checkingof the resulting model family using variability-specific abstraction refinement, so that only those variants (family members) that satisfy the given LTL properties represent “correct” realizations of the given model sketch. We have implemented a prototype model synthesizer for resolving Promelasketches. It calls the spinmodel checker for verifying Promelamodels. We illustrate the practicality of this approach for synthesizing several Promelamodels. |
Full text from SpringerLink