About
Aitartos is a tool for Automatic Implementation of Timed Automata model in a Real-time Operating System.
The purpose of this tool is to make design, implementation and verification of real-time control systems easier because human resources will be concentrated more on the area of specification and verification than implementation issues.
Aitartos includes developed modules enabling automatic implementation of Timed Automata models from UPPAAL into the real-time operating system extension RTX.
The software tool is being developed with the support from the National Grant Agency at the Department of Control and Instrumentation, Brno University of Technology.
Implementation of the Timed Automata model in RTX can be carried out automatically in the Aitartos. The relationship between UPPAAL, Aitartos tool, RTX, x86 target platform and control technology is shown in the following figure.
The Model of the control system is created and verified in the UPPAAL tool. If the verification is passed then the implementation tool reads the Timed Automata model saved in XML file and creates a Visual C++ project for the RTX application. The RTX application creates one task consisting of one or more threads. Each thread in the RTX process is equivalent to UPPAAL process assignment. The RTX process has a direct connection to the Hardware Abstraction Layer (HAL) of the Target Platform and it can directly control hardware in the Technology. Mapping of the model variables into the hardware must be completed by a human in Visual C++ project. However internal behaviour of the RTX process and its threads are generated automatically by Timed Automata model.
Many problems must be solved before the Timed Automata model can be successfully transferred into the RTX structures. The most important one is a time concept. UPPAAL time is an integer value passing from –∞ to +∞. RTX time is based on a HAL timer period that is a minimum time quantum that can be used for timers and sleep functions. This HAL timer period can be one of the fixed value; 100, 200, 500 and 1000 us and this value is the same for all processes and its threads. The corresponding value must be chosen before the implementation of the Timed Automata in RTX as the implementation tool should be aware of it.
Another problem can be with the Urgent Channels. Urgent channels are similar to synchronisation channels, except that it is not possible to delay in the source state if it is possible to trigger a synchronisation over an urgent channel. It cannot be successfully realized in symmetric architecture with one available CPU (with just one core) in the target platform. Therefore, urgent synchronization is carried out by a supervising thread using the maximum priority. This thread is attached to the control process and controlled via the HAL timer period.
