DCSYNTH v1.0

Case Studies

Amol Wakankar, Paritosh K. Pandya and Raj Mohan Matteplackel

  • Robustness
  • Shield Synthesis
  • Latency


  • Robustness

    To illustrate the application of soft requirements we synthesize robust controllers for the following notions of robustness for a 4 cell arbiter using DCSYNTH v1.0. The results are tabulated in Table. 3 in the report. Tar ball of source files for all our experiments on robustness can be found 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 experiments 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 Burst error shield synthesis can be found here.

    The AMBABUS requirements for our experiments are taken from Bloem et. al. [BKKW15] Table. 1. For example, in our experiments when we say G1+2+3 we mean the conjunctions of guarantees G1, G2 and G3 in the table.

    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. A report on these can be found on the page here.


    Latency Measurement

    Our experiments on latency measurement includes several variants of two example specifications - minepump and arbiter. Tar ball of source files for each our experiments on latency measurement can be found below here. Each tar ball has a HowToRun file, it gives how to synthesize a controller in (SCADE or NuSMV) from a specification file and do the performance measurement. You can use simchro to simulate the controllers synthesized by DCSYNTH v1.0.


    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 BARC, Mumbai, India.


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