autocode4 online with Winfy

We have hosted the application autocode4 in order to run this application in our online workstations with Wine or directly.

Quick description about autocode4:

autoCode4 is an engine that synthesizes controllers from formal specifications described under a subset of linear temporal logic (LTL).

Importantly, it synthesizes synchronous dataflow controllers (in Lustre or in Ptolemy II form) and maintains requirement-to-code traceability. Such feature is mandated in developing safety-critical systems and are considered essential for specification validation or integrating manual implementation such as legacy code.

The LTL specification captures the desired behavior of a controller where the environment takes the first move (i.e., sense/input then react/output), so the synthesized controller can be viewed as a Mealy machine.

A step-by-step tutorial is available within the software package.

Features:

• Control synthesis from formal specification
• Produce requirement-to-module traceability report

Audience: Aerospace, Information Technology, Science/Research, Manufacturing, Developers.
User interface: Console/Terminal, Command-line.
Programming Language: Java.

.