Averest

Last updated

Averest is a synchronous programming language and set of tools to specify, verify, and implement reactive systems. [1] [2] It includes a compiler for synchronous programs, a symbolic model checker, and a tool for hardware/software synthesis.

Contents

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.

See also

References

  1. ↑ 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.
  2. ↑ 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.
  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.


This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.