PV2 autoCode4synthesises a reactive controller based on requirements written in the GXW subset of LTL

autoCode4 synthesizes structured reactive controllers from realizable specifications in the GXW subset of linear temporal logic (LTL)

Application domain/field

Type of tool

Reactive controller synthesizer

Expected input

Expected output

Reactive controller as a Ptolemy II model. From this model one can automatically generate executable C or HDL code. autoCode4 can also generate reactive controllers in Lustre.

Internals

autoCode4 maintains traceability between individual requirements and the generated controller blocks.
Synthesis

Links

Code: https://sourceforge.net/projects/autocode4/

Last commit date

Last updated: 20 October 2016 on sourceforge

Related papers

https://doi.org/10.1007/978-3-662-54577-5_23 (TACAS '17)

Last publication date

31 March 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.