Uppaal for Testing Real-time systems ONline v.1.4 for Linux ------------------------------------------------------------- Uppaal License -------------- We (the licensee) understand that UPPAAL includes but is not limited to the programs: uppaal2k.jar, uppaal, uppaal.bat, server, socketserver, atg2ugi, atg2ta, atg2hs2ta, hs2ta, checkta, simta, verifyta, tron, uppaal, and xuppaal and that they are supplied "as is", without expressed or implied warranty. We agree on the following: 1. You (the licensers) do not have any obligation to provide any maintenance or consulting help with respect to UPPAAL. 2. You neither have any responsibility for the correctness of systems verified using UPPAAL, nor for the correctness of UPPAAL itself. 3. We will never distribute or modify any part of the UPPAAL code (i.e. the source code and the object code) without a written permission of Wang Yi (Uppsala University) or Kim G Larsen (Aalborg University). 4. We will only use UPPAAL for non-profit research purposes. This implies that neither UPPAAL nor any part of its code should be used or modified for any commercial software product. In the event that you should release new versions of UPPAAL to us, we agree that they will also fall under all of these terms. NEW in this Release ------------------- - Textual communication via standard I/O adapter (see tracer example). - TCP/IP socket adapter for remote IUTs. - Java adapter framework with virtual and real-time support. - Check for correct system model partitioning by input/output channels. Software requirements --------------------- - Platform: Linux 2.4.x or 2.6.x on Intel PC. - Optional: GNU tools: make, g++ (version 4.x recommended) for C-libs. - Optional: Java 5 (or 6) for java examples. - Optional: DOT/graphviz and GhostView (gv) for displaying the signal flow and partitioning of the system model (see "tron -i dot"). Contents -------- - tron Uppaal TRON executable ELF binary for Linux on Intel PC. - java Java examples. Currently contains smart-lamp controller example with Java Socket adapter, available in real-time and virtual time. - include Header files necessary for building dynamic C-library adapter (and back-linking to virtual time symbols in TRON executable). - button Mouse button example containing dynamic link C library adapter. Test setup available for both virtual and real-time testing. - latency Experiments evaluating TRON's input scheduling latency. - tracer A test suite against TRON, testing a few Uppaal modeling features using TraceAdapter interface (in virtual time). Serves as a TraceAdapter example which implements textual communication with TRON. Assumes that GNU make and bash are available for manipulation of various traces in different setups (see tracer/Makefile). Brief Usage ----------- - Type "make help" to see the available targets. - Check the contents of java/README.txt on how to run smart-lamp example. There's also javadoc available: java/doc/index.html. - To see the signal flow of system model and partitioning in testing use the "-i" option ("-v 3" is useful when experimenting). The following produces the system model signal flow diagram: "../tron -i dot LightContr.xml -I TraceAdapter < LightContr.trn > signalflow.dot" The following will produce PNG picture of the signal flow diagram: "dot signalflow.dot -Tpng -o signalflow.png" The legend of the diagram: environment-controlled entities are in green, IUT entities are in blue; ellipse means a process, diamond -- a channel, rectangle -- data variable. Arrows denote a signal flow. For a detailed usage look at output of "tron -h", check the related examples, read publications about TRON/T-Uppaal. Perhaps there'll be thesis about it soon. You are encouraged to try the Linux version which has a few more examples. If you are planning to use it for your research paper, I would be more than happy to help. Bugreports are welcome at: http://bugsy.grid.aau.dk/cgi-bin/bugzilla/index.cgi Written, built and maintained by Marius Mikucionis in close collaboration with: Brian Nielsen , Kim Guldstrand Larsen and last but not least, based on the work by Uppaal Team http://www.uppaal.org/