DCSYNTH v1.0

Guided Reactive Synthesis with Soft Requirements for Robust Controller and Shield Synthesis

Amol Wakankar, Paritosh K. Pandya and Raj Mohan Matteplackel

  • Introduction
  • arXiv Report
  • Distribution, Installation and User Manual
  • Case Studies
  • Shield Synthesis
  • References and Lecture Notes/Slides
  • Some Links of Interest


  • Introduction

    Quantified Discrete Duration Calculus (QDDC) is a highly succinct interval temporal logic for specifying safety and bounded liveness properties of reactive systems. In this project, we propose soft requirements with priorities as a technique to guide the controller synthesis from QDDC specifications in a locally optimal fashion, and the tool DCSYNTH v1.0 which implements this technique. Soft requirements provide an invaluable ability to guide the controller synthesis as they can affect the quality of the controller and allow robust (best effort) controllers to be specified. In DCSYNTH v1.0synthesis, hard requirements must be invariantly satisfied whereas soft requirements may be satisfied as much as possible in a best effort manner by the controller. Using the tool, we show the application of soft requirements in synthesizing robust controllers with various specifiable notions of robustness as well as efficient runtime enforcement shields which can correct burst errors. Soft requirements are also handy in improving the latency of controlled system. We illustrate our method and DCSYNTH v1.0 by analyzing the impact of various soft requirements in a synchronous bus arbiter and a pump controller case studies.

    The controller synthesized by DCSYNTH v1.0 can be translated into any target programming/specification language. DCSYNTH v1.0 supports two target languages - SCADE/Lustre and NuSMV.

    Acknowledgements: DCSYNTH v1.0 uses DCVALID 2.0, the model checker for QDDC formulae, and MONA 1.4, the validity checker for WS1S formulae developed at Aarhus University, Denmark. We are grateful to designers of these softwares for permission to use them for the development of DCSYNTH v1.0.


    Distribution: DCSYNTH v1.0 (released on 24 October, 2017).

  • DCSYNTH v1.0 x64_linux distribution for Intel PC.
  • DCVALID 2.0 linux-elf distribution for Intel PC. Required by DCSYNTH v1.0, includes the distribution MONA 1.4.
  • Lustre V4 Toolbox. Recommeded. The distribution includes simchro for simulation of SCADE synthesized by DCSYNTH v1.0.
  • NuSMV. Required for Latency Measurement Experiments.
  • DCSYNTH v1.0 is available free of cost for educational use. See LICENSE before downloading.

    Please send me an email if you download this software.
    This will allow me to notify you about new releases and changes.

    Installation and Usage

    DCSYNTH v1.0

    You can use simchro to simulate the controllers synthesized by DCSYNTH v1.0.

    DCVALID 2.0


    Case Studies

    Using DCSYNTH v1.0, we have done experiments showcasing the application of soft requirements in synthesizing robust controllers with various specifiable notions of robustness, runtime enforcement shields, and controllers with improved latency. Details of these experiments as well as source files can be found on the page here.

    Robustness

    We consider various notions of robustness. Tar ball of source files for our experiments on robustness can be found on the page here.

    Shield Synthesis

    Shield synthesis criteria can be specified using hard and soft requirements. DCSYNTH v1.20 can then synthesize the desired shield. We give examples of conservative K-shield and conservative Burst error shield which are variants of K-shield of Bloem et. al. [BKKW15] and Burst error shield of Wu et. al. [WWZ16] respectively. Tar ball of source files for our experiments on conservative shield synthesis can be found on the page here.

    NEW !!! We have added the shield synthesis for the following shield criteria. Tar ball of source files for our experiments on these can be found on the page here.

    Latency Measurement

    Soft requirements are often used as directives to the synthesis algorithm which impact the latency of the controller. Our experiments on latency measurement includes several variants of two example specifications - minepump and arbiter. Tar ball of source files for our experiments on latency measurement can be found on the page here.


    References

  • [MPW17] Raj Mohan Matteplackel, Paritosh K. Pandya and Amol Wakankar: Formalizing Timing Diagram Requirements in Discrete Duration Calculus. SEFM 2017.
  • [Pan01a] Paritosh K. Pandya: Specifying and Deciding Qauntified Discrete-time Duration Calculus formulae using DCVALID. RTTOOLS 2001.
  • [Pan01b] Paritosh K. Pandya: Model checking CTL[DC]. TACAS 2001.
  • [BKKW15] Roderick Bloem, Bettina Könighofer, Robert Könighofer and Chao Wang: Shield Synthesis: Runtime Enforcement for Reactive Systems. TACAS 2015.
  • [WWZ16] Meng Wu, Haibo Zeng and Chao Wang: Synthesizing Runtime Enforcer of Safety Properties Under Burst Error. NFM 2016.
  • [BGJPPW07] R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli and M. Weiglhofer: Automatic Hardware Synthesis from Specifications: A Case Study. DATE 2007.
  • Lecture Notes/Slides

  • Slides on DCSYNTH v1.0, presented at ATVA 2017, Pune, India.
  • Slides on DCSYNTH v1.0, presented at BARC, Mumbai, India.
  • Slides on DCSYNTH v1.0, presented at IIT Guwahati, India.
  • Formalizing Timing Diagram Requirements in Discrete Duration Calculus, presented at SEFM 2017, Trento, Italy.

  • Some Links of Interest

  • MONA - a validity checker for WS1S.
  • DCVALID 2.0 - Model checker for QDDC formulae.
  • SMV and NuSMV.
  • simchro.
  • Jonathan Bowen's Formal Methods Page.
  • Formal Methods in India.



  • This page was created by Paritosh K. Pandya on 24 October, 2017.