Navigationsmenü

Sie sind hier: Uni . Fk. II . Informatik . theoretica . CSD . Teaching . FP. Realzeitsysteme . Result

Correct System Design

Practical course ``Real-Time Systems''

Final report

1 Introduction

The practical course for advanced students with the topic "Real-Time Systems" took place in the winter term 2000/2001 at the Carl-von-Ossietzky University of Oldenburg under supervision of Dr. Henning Dierks. Five students joined the class (see participants) and splitted into two groups for the first meetings.

In real-time systems, the time in which certain actions must be executed, plays an important role. For example, machines must react within a certain time bounds to external events (for instance sensor data). In the practical course we learned how one can model and verify such systems. Additionally real time programs for Lego Mindstorms robots were simulated and implemented. For the Lego Mindstorms controller (so-called "RCX") there exists a free operating system named LegOS which can execute C-programs. These programs were written either "by hand" or generated by Moby/PLC (a design tool for distributed real-time control programs running on programmable logic controllers).

2 Topics of the practical course

In the first three exercises the hardware platform (RCXes with LegOS) was introduced. C-Programs were developed, compiled and executed on the RCXes. Communication between two RCXes was established using the remote infrared interface.

The programs were formally verified by using Uppaal. The systems were modelled as timed automata in the appropriate syntax and then checked by Uppaal for certain desirable properties.

Then the tool Moby/PLC was used. With this tool, real-time programs given as PLC-Automata can be graphically modelled and simulated. It can generate both LegOS- as well as Uppaal-code automatically, so that then the systems can be verified by means of Uppaal and executed on the RCXes.

At the end of the practical course a complex final project was solved by all participants.

3 Final project

The task consisted of designing a track system from Lego rails, on which two Lego trains (two RCXes) are to drive. A critical area, which both trains can enter, should be controlled as flexible as possible by a rail switch system (two further RCXes). As an additional function it should also be permitted for a train to change its driving direction within the critical area. The command for this behaviour can be issued by a remote control. The following pattern was designed:

At the green circles touch sensors located on the train are activated, whereupon it slows down and stops at the light signals (red circles) of the rail switch (the way from the touch sensor to the signal is determined by means of a rotation sensor). The activation of the signal by the switch control is recognised by a lightsensor on the train which then enters the critical area. In the places marked blue touch sensors are activated by passing trains. Thus the position of the train can be determined by the switch control. Since both switches must know both train positions, infrared communication between the two RCXes is established ("IR" area). Thus all LegOS knowledge from the previous exercises could be applied in this project.

track system I

track system II

track system III

The first problems already occurred at the construction of the hardware from Lego elements. While the switch control could be built quite easily, we had to try out a lot of alternatives for the trains. Since the RCXes are quite heavy, the power of the engines had to be transferred very efficiently to the train wheels. It was necessary to strengthen the drive unit by many tie bars. However the trains were not allowed to become too broad (the distance between the rails was relatively small) nor too high (the train would turn over in the curves). Afterwards we needed to design the sensors along the rails. As a substantial aid rubber bands were used. They become strained by a lever, which is moved by the passing train, and then presses a Lego brick against the touch sensor. Similarly the touch sensors at the trains were constructed.

switch control

touch sensor (

)

train drive system

As a further function we had to verify the developed programs by means of Uppaal. The control programs of the trains were developed directly in C, so we had to write the Uppaal input directly, too. The switch control program however was created with Moby/PLC. The generated Uppaal-code could be completely verified despite its complexity due to safe abstractions. Here the real time aspect shows up very clearly: Due to their construction touch sensors are released only for a short period of time, whereas the RCXes of the switch control have a cycle time of 600ms which is caused by the slow IR communication. Therefore it can occur that a passing train is not recognised correctly by the switch controllers. If these controllers discover such a "lost" train later on when it passes other touch sensors in the field, then the controllers switch into an error state.