Download
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
Project Samples
License
GNU Library or Lesser General Public License version 3.0 (LGPLv3)Follow autoCode4
Other Useful Business Software
Our Free Plans just got better! | Auth0
You asked, we delivered! Auth0 is excited to expand our Free and Paid plans to include more options so you can focus on building, deploying, and scaling applications without having to worry about your security. Auth0 now, thank yourself later.
Rate This Project
Login To Rate This Project
User Reviews
Be the first to post a review of autoCode4!