DCSynth: Guided Reactive Synthesis with Soft Requirements and Performance Measurement

Amol Wakankar, Paritosh K. Pandya and Raj Mohan Matteplackel

  • Introduction
  • Distribution, Installation and User Manual
  • Examples
  • Technical Reports 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 a technique and the tool DCSynth v1.0 for automatic controller synthesis from a QDDC specification. Our technique allows a set of (temporal) soft requirements with priorities to guide the controller synthesis in a locally optimal fashion (implemented in DCSynth). Clearly, these soft requirements affect the quality of the controller, and they allow robust (best effort) controllers to be specified. DCSynth implements a symbolic model checking technique for exactly computing the worst-case performance of a controlled system where the performance is specified as the maximal span of a QDDC formula. We illustrate our method and the tool DCSynth 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 08 May, 2017).

  • 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.
  • 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


    Examples


    Technical Reports

  • Raj Mohan Matteplackel, Paritosh K. Pandya and Amol Wakankar: Formalizing Timing Diagram Requirements in Discrete Duration Calculus. Available at https://arxiv.org/abs/1705.04510.
  • Paritosh K. Pandya: Specifying and Deciding Qauntified Discrete-time Duration Calculus formulae using DCVALID. In Proc. Real-Time Tools, RTTOOLS 2001.
  • Paritosh K. Pandya: Model checking CTL[DC]. In Proc. TACAS 2001.
  • Lecture Notes/Slides

  • Slides on DCSynth v1.0, presented at BARC, Mumbai, India.

  • 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 08 May, 2017.