A formal design and implementation method for real-time embedded systems

This paper tackles the problem of using formal meth-ods for practical real-time system development and ver-i cation, and is based on a real example. Many formal methods for real-time systems have been proposed, but this technique (AORTA) is one of the few to address the issue of how formal designs are to be implemented. Earlier papers on AORTA have been based on providing the formal semantics of the language, and on particular aspects of implementation or verication. This paper concentrates on setting AORTA within the development life cycle, and demonstrating that the approach can be adopted for non-trivial examples. 1