Citation
Chihhong Cheng, Edward A. Lee, Harald Ruess. "autoCode4: Structural Controller Synthesis". To appear in Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, 22, April, 2017.

Abstract
autoCode4 synthesizes structured reactive controllers from realizable specifications in the GXW subset of linear temporal logic (LTL). Generated reactive controllers are expressed in terms of an intermediate synchronous dataflow (SDF) format, which is further translated, using an open interface, into SCADE/Lustre and Ptolemy II. Moreover, autoCode4 generates and maintains a traceability relation between individual requirements and generated code blocks, as mandated by current standards for certifying safety-critical control code. 1

Electronic downloads

• ChengEtAl_AutoCode4_TACAS17.pdf · application/pdf · 586 kbytes

• HTML

  Chihhong Cheng, Edward A. Lee, Harald Ruess. <a
  href="http://chess.eecs.berkeley.edu/pubs/1186.html"
  >autoCode4: Structural Controller Synthesis</a>,
  <em>To appear in </em>Proceedings of the
  International Conference on Tools and Algorithms for the
  Construction and Analysis of Systems (TACAS), Springer, 22,
  April, 2017.

• Plain text

  Chihhong Cheng, Edward A. Lee, Harald Ruess.
  "autoCode4: Structural Controller Synthesis".
  <em>To appear in </em>Proceedings of the
  International Conference on Tools and Algorithms for the
  Construction and Analysis of Systems (TACAS), Springer, 22,
  April, 2017.

• BibTeX

  @inproceedings{ChengLeeRuess17_AutoCode4StructuralControllerSynthesis,
      author = {Chihhong Cheng and Edward A. Lee and Harald Ruess},
      title = {autoCode4: Structural Controller Synthesis},
      booktitle = {<em>To appear in </em>Proceedings of the
                International Conference on Tools and Algorithms
                for the Construction and Analysis of Systems
                (TACAS)},
      organization = {Springer},
      day = {22},
      month = {April},
      year = {2017},
      abstract = {autoCode4 synthesizes structured reactive
                controllers from realizable specifications in the
                GXW subset of linear temporal logic (LTL).
                Generated reactive controllers are expressed in
                terms of an intermediate synchronous dataflow
                (SDF) format, which is further translated, using
                an open interface, into SCADE/Lustre and Ptolemy
                II. Moreover, autoCode4 generates and maintains a
                traceability relation between individual
                requirements and generated code blocks, as
                mandated by current standards for certifying
                safety-critical control code. 1},
      URL = {http://chess.eecs.berkeley.edu/pubs/1186.html}
  }
  

Posted by Mary Stewart on 13 Jan 2017.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.