A Framework for Verifying and Implementing Embedded Systems.
Klaus Schneider, Tobias Schüle · 2006
We present a framework for the development of embedded systems called Averest. It includes a compiler for synchronous programs, a symbolic model checker, and a tool for hardware and/or software synthesis. Averest can be used for modeling and verifying finite as well as infinite state systems. Thus, Averest is not only well–suited for hardware design, but also for the develop-ment of embedded software. In particular, our input language Quartz allows the description of concurrent programs at a high level of abstraction. 1