Application Oriented RealTime Algebra
AORTA (Application Oriented
RealTime Algebra) has been developed to provide a
formal language for the engineering of hard realtime systems. AORTA
is a timed process algebra, but differs from other such algebras in
its semiautomatic 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
modelchecking 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
Papers
To date, the following papers have been written on AORTA:

Practical Formal Development of RealTime Systems
11th IEEE Workshop on RealTime Operating Systems
and Software, RTOSS '94, Seattle

ApplicationOriented RealTime Algebra
Software Engineering Journal 9(5), September 1994,
pp201212

Designing and Implementing Correct RealTime Systems
Formal Techniques in RealTime and FaultTolerant
Systems FTRTFT '94, Lubeck, Lecture Notes in Computer Science 863,
pp228246

A Formally Based Hard RealTime Kernel
Microprocessors and Microsystems 18(9), November 1994,
pp513521

Validation, Verification and Implementation of Timed Protocols using
AORTA
Protocol Specification, testing and Verification XV (PSTV '95),
Warsaw, June 1995

A Formal Design and Implementation Method For RealTime Embedded Systems
22nd Euromicro conference (Euromicro '96), Prague, September 1996

Integrating AORTA with ModelBased Data Specification Languages
Fundamental Approaches to Software Engineering FASE '98,
Lecture Notes in Computer Science 1382, pp5471

Formal Methods and Tool Support for RealTime Presented at
IEE Colloquium on RealTime Systems, University of York, April 1998
Steven Bradley's thesis
An
Implementable Formal Language for Hard RealTime Systems is also available.
The AORTA toolset
As part of the project, a toolset is being developed to provide
computer support for formal realtime system development. To date, the
toolset includes
 A parser and static semantic checker for annotated AORTA designs
 A C and assembly language code generator suitable for use with
the AORTA kernel and VxWorks
 A design simulator, on similar lines to the simulator in the
Edinburgh concurrency
workbench
 A facility for displaying graphical layouts of AORTA systems,
interfaced with behaviour simulator. Click here for a screen
dump of the simulator in action on the alternating bit protocol.
 A timed graph generator, interfaced with the KRONOS tool
(produced by Sergio Yovine
who works at
CNRS as part of the
SPECTRE
project), for timed modelchecking. There is also a tool for
graphical display of the timed graphs generated, based on Tcl/Tk.
Work is currently underway on providing a more efficient (dedicated)
modelchecker. 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: +441913743654