Averest is a synchronous programming language and set of tools to specify, verify, and implement reactive systems.12 It includes a compiler for synchronous programs, a symbolic model checker, and a tool for hardware/software synthesis.
It can be used to model and verify finite and infinite state systems, at varied abstraction levels.3 It is useful for hardware design, modeling communication protocols, concurrent programs, software in embedded systems, and more.
Components: compiler to translate synchronous programs to transition systems, symbolic model checker, tool for hardware/software synthesis. These cover large parts of the design flow of reactive systems, from specifying to implementing. Though the tools are part of a common framework, they are mostly independent of each other, and can be used with 3rd-party tools.
References
References
- Rafique, Omair; Gesell, Manuel; Schneider, Klaus (August 2013). "Targeting different abstraction layers by model-based design methods for embedded systems: A case study". 2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications. pp. 334–337. doi:10.1109/RTCSA.2013.6732235. ISBN 978-1-4799-0850-9.
- Huss, Sorin Alexander (2007-07-19). Advances in Design and Specification Languages for Embedded Systems: Selected Contributions from FDL'06. Springer Science & Business Media. pp. 245–246. ISBN 978-1-4020-6149-3.
- Butler, Michael; Hinchey, Michael G.; Larrondo-Petrie, Maria M. (2007-10-27). Formal Methods and Software Engineering: 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, Florida, USA, November 14-15, 2007, Proceedings. Springer. p. 91. ISBN 978-3-540-76650-6.
External links
External links
- Averest Toolbox Official home site
- Embedded Systems Group Research group that develops the Averest Toolbox