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.

DCSYNTH v1.0 is available free of cost for educational use. See LICENSE before downloading.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.

*Please send me
an email
if you download this software.*

This will allow me to notify you about new releases and changes.

- Installation notes are in
file contained in the distribution.__install.readme__ **User manual :**the documentation is contained in the user manual UserManual.pdf.-
Includes several case studies.
The documentation on how to run DCSYNTH v1.0 on the examples can be found in
in the distribution.__examples.readme__

- Installation notes are in
file contained in the distribution.__INSTALL.README__ **User manual :**the documentation is contained in the user manual dcvalid.txt.

**Be-Correct**If assumption has held invariantly so far then commitment must hold now.**Be-Currently-Correct**If assumption holds intermittently, the commitment must hold whenever assumption holds.**Degraded-Performance**Let Ad ⊆ A and Cd ⊆ C, where A, C denote set of assumptions and commitments, and Ad, Cd denote reduced set of assumptions and commitments which specify degraded behaviour of system when fewer assumptions hold.**Never-Give-Up**In addition to Be-Correct, all the commitments are asserted as soft requirements. This makes the controller synthesizer attempt to make them true even when assumptions do not hold, and for as many inputs as possible.**Greedy**Here commitments are given as soft goals ignoring the assumptions. The synthesis algorithm tries ot make as many commitments true as possible at each step in a greedy fashion.**k-Bounded**If in past assumptions have been violated at most*k*times so far then commitment must be met.**k,b-Resilient**A subinterval where assumption is continuously true for*b*or more cycles is called a recovery period. It states that between any two recovery periods, the maximum number of assumption violations is at most*k*.**k,b-Variant**If in past in any period of length*b*the assumption has been violated at most*k*times then the commitment must hold.

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.

**Conservative burst error shield**- Input: I ∪ O. Output: O1.

- Hard requirement: REQ[O/O1].

- Soft requirement: ∀o∈O: (true ^ <o=o1>).

**Conservative k-shield-V1**- Input: I ∪ O. Output: O1.

- Hard requirement: REQ[O/O1] &&[]([[∃o∈ O:(o≠o1]]=>slen<k).

**Conservative k-shield-V2**- Input: I ∪ O. Output: O1.

- Hard requirement: REQ[O/O1]&&[]([[ind && ∃o∈O:(o≠o1)]]=>slen<k).

- Indicator ind : REQ(I,O).

**Conservative k-shield-V3**- Input: I ∪ O. Output: O1.

- Hard requirement: REQ[O/O1]&&[]([[ind && ∃o∈O:(o≠o1)]]=>slen<k)|.

- Indicator ind : ∃O2.((([O2=O1] || pt)^<O2=O>) && REQ(I,O2).

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

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.

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