University of Leicester
Browse
repair.pdf (462.11 kB)

Symbolic repairs for GR(1) specifications

Download (462.11 kB)
conference contribution
posted on 2019-06-20, 08:41 authored by Shahar Maoz, Jan Oliver Ringert, Rafi Shalom
Unrealizability is a major challenge for GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis. Some works attempt to help engineers deal with unrealizability by generating counter-strategies or computing an unrealizable core. Other works propose to repair the unrealizable specification by suggesting repairs in the form of automatically generated assumptions. In this work we present two novel symbolic algorithms for repairing unrealizable GR(1) specifications. The first algorithm infers new assumptions based on the recently introduced JVTS. The second algorithm infers new assumptions directly from the specification. Both algorithms are sound. The first is incomplete but can be used to suggest many different repairs. The second is complete but suggests a single repair. Both are symbolic and therefore efficient. We implemented our work, validated its correctness, and evaluated it on benchmarks from the literature. The evaluation shows the strength of our algorithms, in their ability to suggest repairs and in their performance and scalability compared to previous solutions.

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).

History

Citation

Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, 2019, pp. 1016-1026

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Informatics

Source

ICSE '19 Proceedings of the 41st International Conference on Software Engineering, Montreal, Quebec, Canada

Version

  • AM (Accepted Manuscript)

Published in

Proceedings of the 41st International Conference on Software Engineering

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Copyright date

2019

Available date

2019-06-20

Publisher version

https://dl.acm.org/citation.cfm?id=3339632

Notes

SYNTECH: http://smlab.cs.tau.ac.il/syntech/

Temporal coverage: start date

2019-05-25

Temporal coverage: end date

2019-05-31

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC