LEGO® meets RV—Distributed Runtime Verification on Embedded Systems
The project LEGO® meets RV is an implementation of distributed runtime verification for LEGO® Mindstorms NXT robots. The robots are programmed using the C-dialect Not eXactly C (NXC). In the source code you can add special comments which are parsed by the preprocessor developed in this project and freely available on this page. These special comments contain correctness properties which will be verified by monitors generated out of the annotations. To specify the properties the Distributed Temporal Logic (DTL) is used. This logic is based on (pt)LTL but contains the additional @-operator which specifies on which agent a subformula should be evaluated.
Case Study: Assembly Line
This case study is an example of the usage of the distributed runtime verification developed in this project. An assembly line controlled by four communicating agents is used as example for an asynchronous distributed system. A work piece is moved by conveyors and a revolving table through the assembly line, which is controlled by four NXT agents communicating via Bluetooth. The picture above shows the schematic layout of the four NXT agents in the assembly line. The work piece starts at conveyor B1 controlled by agent Z1 via motor A. Sensor 1 denotes a work piece on the conveyor in front of the sensor and output C is used to indicate the status of a monitor attached to this agent. On the revolving table T the work piece is rotated and moved onto conveyor B3 by the slider K.
The following video shows some runs of the system. The correctness of the system is verified using two different properties expressed in DTL.
Watch the video on YouTube. (Dieses Video auf deutsch bei YouTube ansehen.)
Appetizer
Consider the following property in the above setup.
This formula demands that sensor 1 at agent A does not recognize a work piece until sensor 1 at agent Z2 sees one. This asserts that no work piece appears on the revolving table that has never been on the conveyor in front of the revolving table.
1. Name the agents
The source code of every agent of the system needs an annotation giving this agent an unique name. On agent A this is
//= AGENT output
and on agent Z2 this is
//= AGENT input2
2. Declare propositions
Propositions have to be declared before they can be used in formulas. On both agents we need a proposition s1 defined as follows:
//= PROPOSITION s1 DEFINE (Sensor(S1) >= WHITE_STONE)
As the remote subformula becomes a remote proposition we need to define the following external proposition on agent A (output)
//= PROPOSITION i2 EXTERNAL input2
3. Declare monitors
Using this propositions we can now declare the main monitor on agent A (output) as follows
//= MONITOR bb FDTL=!s1 U z2
The referenced remote subformula has to be declared on its agent Z2 (input2) separately as follows
//= PUBLIC MONITOR i2 PTDTL=s1
This monitor is declared public as it is referenced as remote proposition.
4. Declare events
Events are used to define the point in time at which the monitor should evaluate the next step. This is an important part in the definition, because LTL is defined for discrete sequences of states and real world systems are not discrete. For the monitor bb on agent A (output) we add
//= EVENT bb CHANGE s1 //= EVENT bb CHANGE z2
and for the monitor i2 on Z2 (input2) we add
//= EVENT i2 CHANGE s1
These events define that the monitor evaluates a new state with every change of any proposition contained in the formula.
Publications and Further Information
The logic DTL and its autmata construction are described in our paper Three-Valued Asynchronous Distributed Runtime Verification. Much more details on the syntax and semantics of the annotations and DTL can be found in the (german) master thesis of Malte Schmitz.
Usage
To compile the annotations into monitors pass all NXC source files of the system to the preprocessor at once.
java -jar legomeetsrv.jar output.nxc table.nxc input1.nxc input2.nxc
This will generate an output file ending with _out.nxc for every input file and information for every monitor generated for the purpose of debugging. If you dot not want these debugging files pass the extra option --silent.
The NXC output source files now need to be compiled and copied onto the NXC agents individually. This can be done using the NBC compiler written by John Hansen using the following command.
nbc table_out.nxc -r nbc input2_out.nxc -r nbc input1_out.nxc -r nbc output_out.nxc -r
The option -r tells the compiler to download and run the compiled byte code on the agent connected via USB or Bluetooth to the computer.
The monitors generated are cached in the SQLite database cache.db. This cache is only used to improved the performance and can be safely deleted.
Download
The archive contains the examples discussed in the video and the jar archive containing the compiled source with all dependencies. The dependencies in detail are: Scala Standard Library, db4objects, LamaConv and Reduce. You need at least Java 1.6 to run the code.
Contact
If you have further questions, problems using the software provided on this page or want to extend it in some way, feel free to contact Torben Scheffel or Malte Schmitz.
OR.NET
The project LEGO® meets RV was undertaken partly in the scope of our engagement in the project OR.NET.