Loading...
Please wait, while we are loading the content...
Similar Documents
Verifying Distributed LEGO RCX Programs Using UPPAAL
| Content Provider | Semantic Scholar |
|---|---|
| Author | Laursen, Morten Madsen, Rune G. Kondrup, Steffen Traisathit, Patrinee |
| Copyright Year | 1999 |
| Abstract | In this article we show a way to model and verify programs running on LEGO RCX bricks using the tool U PPAAL. We are able to model two RCX units communicating through an infrared channel. To facilitate the distribution of programs on the two RCXes, we develop the “IR Protocol”, which allows both RCXes to read and write variables and I/O ports on the other RCX. The protocol makes use of a simplified version of Fischer’s mutual exclusion protocol. Both the behavior of Fischer’s protocol and the IR Protocol are verified. It turns out that we have to restrict our models in order to verify anything but very simple programs. A simplified model is shown, and measured to be faster. The IR protocol is demonstrated in a LEGO test setting, and we discuss how to distribute the program controlling it. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.auc.dk/research/FS/teaching/Undergraduate/1999/carticle.ps |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
