Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

LIME Interface Test Bench User Guide Xi Chen, Janne Kauttio, Olli Saarikivi and

LIME Interface Test Bench User Guide Xi Chen, Janne Kauttio, Olli Saarikivi and Kari K¨ ahk¨ onen October 6, 2009 Contents 1 Introduction 2 2 The example program 2 3 Installation and starting up 6 4 Monitoring tools 8 4.1 Opening and compiling the example program . . . . . . . . . . . 8 4.2 Running the example program . . . . . . . . . . . . . . . . . . . 10 4.3 Other monitoring tools . . . . . . . . . . . . . . . . . . . . . . . . 12 4.4 Command-line usage . . . . . . . . . . . . . . . . . . . . . . . . . 14 5 Testing tools 15 5.1 Using Lime Concolic Tester . . . . . . . . . . . . . . . . . . . . . 15 5.2 Limitations of LIME Concolic Tester . . . . . . . . . . . . . . . . 20 5.3 Using JUnit Tools . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.4 Command-line usage . . . . . . . . . . . . . . . . . . . . . . . . . 23 6 Other utilities 23 1 1 Introduction LIME (LightweIght formal Methods for distributed component-based Embedded systems) Interface Test Bench (LimeTB from now on) is a toolkit for testing software components written in Java programming language (limited support for C programming language is also available). With LimeTB, the user can specify behavioral aspects of the software component interfaces as annotations in the source code by using LIME Interface Speciﬁcation Language (ISL). These speciﬁcations can then be automatically monitored for violations during the execution of the program. LimeTB also has tools for automating the testing of a program, and for generating JUnit unit tests. This document introduces the tools provided by LimeTB and how they can be used with the provided graphical user interface. An example program is also introduced that will be used as a running example throughout the guide. The example program is a simple Java program with interface annotations, and will hopefully motivate the reader on how the tools can be useful also in real-life applications. All the LimeTB tools can be used from the user interface and also have a command-line variants that can be used independently. Conventions used in this guide are as follows: • Monospace font will be used for both commands in the graphical user interface as well as command-line commands. • Bold font will be used for diﬀerent ﬁle names throughout the guide. • Italic Italic font will be used to denote names of directories. The guide is structured as follows: In chapter 2 the example program will be presented on a source code level, along with explanations what the diﬀerent parts of the program do. Chapter 3 will go through the initial steps of using the tool, mainly how it’s installed and how the graphical user interface can be started. Chapters 4 and 5 will go through the main features of LimeTB by presenting the tools and how they work with the example program. Finally, Chapter 6 will brieﬂy consider the utilities speciﬁc to the user interface that are designed to make it more usable. In every chapter where a feature of LimeTB is presented, also the equivalent command-line tools will be considered brieﬂy, mainly to let the user know what command does what. 2 The example program In this section the example used during the rest of the guide will be demonstrated in detail with complete source code of all the ﬁles used. The ﬁles will be pre- sented one at a time, each of them followed by notes about what it actually does and what we are trying to achieve. The example program is a simple lock im- plementation that can be locked and unlocked, and an associated main-method that generates one such lock instance and does some operations on it. It should also be noted that this example is also available in the LimeTB/examples/limt- lct/example lock directory in the tool package. 2 package example_lock; import fi.hut.ics.lime.aspectmonitor.annotation.CallSpecifications; @CallSpecifications( regexp = { "StrictAlteration ::= (lock() ; unlock())*" } ) public interface Lock { public void lock(); public void unlock(); } Figure 1: Lock.java In Figure 1 is the interface deﬁnition of a ”Lock” interface. Apart from the extremely simple interface, the only interesting part in this ﬁle is the ”CallSpec- iﬁcations” annotation at the top. This LIME Interface Speciﬁcation Language annotation speciﬁes a spec called ”StrictAlteration”, which basically requires that the calls to methods lock() and unlock() must be done alternately, so a lock that is locked shouldn’t be locked again before it is opened ﬁrst. Remember that this is just one example of what a user can do with Interface speciﬁcations. For more information please check the other examples provided with LimeTB or the speciﬁcation language documentation 1 1Available at http://www.tcs.hut.fi/Software/lime/ 3 package example_lock; public class LockImpl implements Lock { private boolean locked; public LockImpl() { locked = false; } public void lock() { locked = true; } public void unlock() { locked = false; } public boolean getLocked() { return locked; } } Figure 2: LockImpl.java In Figure 2 is shown a class ﬁle that implements the interface in Figure 1. The main thing to note here is that there is no need to write anything special in the classes implementing the interfaces with annotations to make them work with LimeTB tools. 4 package example_lock; public class Main { public void testme (int x, int y) { Lock lock = new LockImpl(); lock.lock(); System.out.println("x = " + x + ", y = " + y); if (x > y) if (x * y == 1452) if (x >> 1 == 5) lock.lock(); lock.unlock(); } public static void main(String[] args) { Main m = new Main(); if (args.length < 2) { System.out.println("please give two integers as arguments"); System.exit(1); } int x = Integer.parseInt(args[0]); int y = Integer.parseInt(args[1]); m.testme(x, y); System.exit(0); } } Figure 3: Main.java Finally in Figure 3 is the main class of the example program. The main method here takes two arguments, and then calls a testme(int, int) method. What this method does is that it ﬁrst creates a ”LockImpl” object (that im- plements ”Lock” interface) and then locks it. Then the method checks if the arguments fulﬁll a speciﬁc criteria (these tests are carefully crafted to only ac- cept certain speciﬁc values for the sake of demonstrating the capabilities of the testing tools) and if they do, the lock is locked a second time, leading to a violation of the speciﬁcation. At the end the method unlocks the lock and exits. As the reader has propably noticed by now, the example doesn’t really do anything useful. It should be noted however, that it demonstrates quite well 5 a case where we have a program with an erroneous execution only with very certain input values. Now imagine a case where such a component is part of some bigger software, and the error could be considerably diﬃcult to locate. Next we’ll go into the installation of LimeTB, and how the user interface can be launched. After that the tools themselves will be presented one at a time. 3 Installation and starting up Installation of LimeTB should be relatively straightforward depending a bit on the system where it’s going to be installed. The tarball LimeTB.tar.gz holds basically everything a user should need to start using the tools, apart from few dependencies. Most of the dependencies are provided in the LimeTB package both as precompiled binaries (for x86 linux) and as source code, but some still need to be installed separately. Dependencies needed by and not provided by LimeTB: Java 1.6: Can be obtained from Sun website 2. ACC: (AspeCt oriented C) only required for using LIMT with C programming language, can be obtained from ACC website 3 (read the installation in- structions carefully). Boolector: Is a SMT-solver used by the test generation tool. It can be down- loaded at Boolector website 4. After downloading Boolector, a shared library used by LimeTB must be compiled. A makeﬁle for this task is provided in the LimeTB/dependencies/solvers/ folder. See the LCT README for more detailed instructions to compiling the library. Yices: Yices is alternative to Boolector and it is available from SRI website 5. The instructions for compiling a shared library for Yices are also given in the LCT README. Dependencies provided by LimeTB: Scheck: In case scheck doesn’t work, necessary sources and patches for recom- pilation are provided in the LimeTB/dependencies directory. Doxygen: Only required for using LIMT with C programming language, sources available under LimeTB/dependencies and precomipiled uploads/S4/ user-guide 40 .pdf