Document Type

Article

Abstract

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well suited for verifying system designs. While Alloy comes deployed in the Analyzer, an automated scenario-finding tool set, writing correct models remains a difficult and error-prone task. ASketch is a synthesis framework that helps users build their Alloy models. ASketch takes as an input a partial Alloy models with holes and an AUnit test suite. As output, ASketch returns a completed model that passes all tests. ASketch's initial evaluation reveals ASketch to be a promising approach to synthesize Alloy models. In this paper, we present and explore SketchGen, an approach that looks to broaden the adoption of ASketch by increasing the automation of the inputs needed for the sketching process. Experimental results show SketchGen is effective at producing both expressions and test suites for synthesis.

Publication Date

7-21-2022

Language

English

License

Creative Commons Attribution 4.0 International License
This work is licensed under a Creative Commons Attribution 4.0 International License.

Download

Share

COinS