Application Oriented Real-Time Algebra

AORTA (Application Oriented Real-Time Algebra) has been developed to provide a formal language for the engineering of hard real-time systems. AORTA is a timed process algebra, but differs from other such algebras in its semi-automatic implementability. Using a dedicated kernel and static object code analysis techniques, guaranteed bounds on performance can be given on the systems that are generated by the AORTA toolset. The formal semantics makes formal verification via model-checking possible, allowing safety properties of concretely realised systems to be proved. There is a tutorial on AORTA , which introduces the notation.

The rest of this page is subdivided as follows


To date, the following papers have been written on AORTA: Steven Bradley's thesis An Implementable Formal Language for Hard Real-Time Systems is also available.

The AORTA toolset

As part of the project, a toolset is being developed to provide computer support for formal real-time system development. To date, the toolset includes Work is currently underway on providing a more efficient (dedicated) model-checker. The toolset is mostly written in standard ML of New Jersey , using Concurrent ML and eXene.

Examples in AORTA

AORTA claims to be `practical' and `implementable', so in order to try to convince you of this fact, we include here a few examples for your perusal, starting small and getting more complicated. Some explanation of the AORTA is given, but links are given to papers which describe the systems in more detail. A tutorial on AORTA is available, which is based on part of a paper.
Page maintained by Steven Bradley
Tel: +44-191-374-3654