Acyclic TeSSLa
Special Fragment. The tools presented on this page are only here for the sake of completeness. They cover the special fragment of acyclic TeSSLa specification, which does not allow recursive specifications. Please refer to the main page for the full TeSSLa and corresponding tool chains.
The Temporal Stream-Based Specification Language (short TeSSLa) was developed in the scope of the CONIRAS project as a specification language. In the CONIRAS project the goal was to use runtime verification techniques early in the development process for debugging multicore systems. Because synthesizing a monitor on an FPGA can take a huge amount of time, it was an important requirement that the elements of a monitor on the FPGA do not have to be synthesized every time a new monitor is created. Instead, a general bunch of elements should be synthesized on the FPGA and only if the elements needed for a TeSSLa specification and their connections do not match to the ones available on the FPGA, a new synthesis process has to be started.
Because the input data for a TeSSLa monitor is supposed to the output of a multicore system, the input is modelled in the form of asynchronous streams. Besides the standard temporal logic operators, TeSSLa contains many other operators like arithmetic ones, timing operators for specifying real-time properties and stream manipulation operations to allow a precise specification of the output streams derived from the input streams.
Tools
This section lists the tools developed by the Institute for Software Engineering and Programming Languages at the University of Lübeck and the IMDEA Software Institute for acyclic TeSSLa.
Compiler
The TeSSLa Compiler takes a TeSSLa specification and translates it into an intermediate representation.
Evaluation Engine
The TeSSLa Evaluation Engine takes an intermediate representation of a TeSSLa specification and a traces and executes the specification on the trace.
The repository also contains several benchmarks used to evaluate the TeSSLaServer. An extended and updated set of benchmarks can be found here.
Online Simulator
The online simulator provides a visualization of TeSSLa input and output streams, which are automatically updated when you change the specification or the input.
Instrumentation
The LLVM instrumentation path can be used to instrument a C program. Such an instrumented C program produces a trace that can be handled by the evaluation engine.
LLVM Instrumentation Path on GitHub
Docker Image
The Docker Image contains all the tools mentioned above.
Docker image with Compiler, Engine and LLVM Instrumentation Pass
TeSSLa Atom Plugin
We integrated all the tools mentioned above into a plugin for the Atom text editor.
TeSSLa Atom plugin in the Atom plugin repository
The following tutorial demonstrates how to use the plugin. In this tutorial we will describe the whole set up process for the TeSSLa Atom package and finally give an example of how to use TeSSLa. Before we are starting with the set up tutorial we will first take a look at TeSSLa, Atom and all other components that are needed to get an environment for developing C programs and TeSSLa specifications.
Introduction
TeSSLa allows users to write formal specifications of program properties that are checked during or after execution of the program. In this tutorial we are using the software instrumentation, so the actual source code that should be checked has to be modified for this purpose. All information that are gathered during execution are based on timestamps. Therefore the observed C functions have to be modified to print logging information to stdout. The logs are stored in a special format as a trace file which is needed by the TeSSLa server as well as the compiled TeSSLa specification to check if the program meets the specification. The TeSSLa specification gets compiled by the TeSSLa compiler.
As you might see in this brief process description there are some components that are essential to be able to use TeSSLa. Now that we have a rough understanding of how the main components are working together we will start with installing all needed components.
Atom and the TeSSLa package
Atom is a text editor that is based on the Electron framework and hence web based. Technically the Atom Editor is a web browser that is encapsulated into a native executable app/program. All add-ons that are developed to increase the range of functions provided by Atom are written in web based programming languages like JavaScript or CoffeeScript and designed in HTML and CSS. As you can imagine it is pretty easy to develop new Atom packages with a good web development background.
Now lets start with installation stuff. First you have to download the latest version of Atom. Therefore visit Atom.io. Directly on the main page there is a 'download' button that will start a download of Atom suitable for the OS you are working on. The actual application is packed into a zip archive. So just unzip the archive with a tool of your choice. When you are working on MacOS you should move the unpacked application to your local applications directory.
Now that we have installed Atom we are taking care of the TeSSLa package. The TeSSLa package adds IDE like functions to Atom allowing developers to use all tools like the TeSSLa compiler, clang and the TeSSLaServer from within Atom. For a developer it is a more comfortable way to verify C code with TeSSLa since all the different tools and commands do not have to be used manually. There are also some helping components that are added to the GUI. For Example a console like component that displays the C programs output and all commands that were executed by the TeSSLa package as well as the responses to these commands. So how do we get this package properly installed on our system?
The good news is that Atom provides a package market place out of the box. Everyone is able to publish own packages on Atom.io and ship updates for them. To get to the market place open Atom and navigate to the preferences pane. Choose the Install section and type in tessla. A list of packages that hopefully contains the wanted one should appear. Press the install button on the tessla package provided by malteschmitz. And that's it. The package gets installed automatically and can be used if the related docker image is available on the system. The next section will provide instructions to get Docker running on your system.
Docker and the TeSSLa-Docker-Image
Ok at this point everything seemed more than less self explanatory. We have already set up the IDE but not the tools that were used by the IDE. You might think: Why do we need Docker for using TeSSLa? We just have a collection of compilers and no special software that is supposed to be executed on a very special OS or an hard to set up environment. Well the key component of the tool chain used by the TeSSLa-Atom-package is the clang with LLVM extensions. The standard clang does not offer these extensions in most cases. For example on MacOS the clang which is part of the command line tools does not support LLVM extensions. The only way to get a clang with LLVM extensions is to build it your self. It turned out that on some systems (especially on Windows) it is nearly impossible to get a working clang with LLVM extensions. The obvious solution for this problem is provided by Docker. Docker provides an environment to run software that is isolated in containers. A Docker container is a kind of lightweight virtual machine. In contrast to virtual machines containers do not bundle full operating systems but only libraries and settings required to make the software work. The key advantage of a Docker container is that it will run regardless on which OS it was started and on each environment it will provide the same functionality. As you might guess it is easy to build the clang with LLVM extensions on a Linux system as for example Ubuntu and isolate it into a Docker container providing an Ubuntu interface. In Addition to the clang compiler the container also contains the TeSSLa-Server and a library for logging purpose.
To be able to run the TeSSLa container we first need to install Docker itself. The safest way to get a working Docker software on your device is to use the official installer from Docker CE. On some systems Docker can be installed using the package manager but in some cases this will end up in a mess since some of the dependencies are not installed directly with the application itself. Anyway go the website linked above and scroll down to the section "Download Docker Community Edition". Choose your OS and download the installer. After the download is done just double click it and install it. If there were no problems the Docker deamon should run in the background now. Now you are able to run Docker containers.
The next step is getting the TeSSLa container. So how do we get this TeSSLa container? There are two ways to get the container. First you can use a Dockerfile to build an image of the TeSSLa container. Run the image and you will get the container. The other way is to get the plain image and just run it. The plain image is hosted on rv.isp.uni-luebeck.de. Download it and and load the image by executing the following commands on command line:
docker rmi tessla
docker load -i tessla
The first command removes other images named 'tessla' that had already been loaded. The second one will load the TeSSLa image so Docker is able to run this image inside of a container. To execute the second command it is important to navigate to the directory that contains the TeSSLa image. When you execute the command in the listing above make sure you are in the directory the TeSSLa image is located in. Now the IDE is able to start a container and execute all commands. If there were no problems so far you are done with setup. All components that are needed are installed and ready to use. The next step is to try it out.
An example application
In this section we will create an example C application and a TeSSLa specification to check if the application meets the specification. Before we start writing code we have to set up a project directory. Open Atom if it is not open yet and go to File – Add Project Folder…. Choose a directory where the new project should be located and press OK.
Now lets add some source files to the newly created project directory. Therefore you can add a new file by right click on the directory in the tree view on the left side of Atom or by using the file menu. We will first create a new C file named sub_add.c. Now put the following content into the C file:
int add(int x, int y) {
return x+y;
}
int sub(int x, int y) {
return x-y;
}
int main() {
int sum = 0;
for (int i = 0; i < 5; i++) {
sum = add(sum, sub(i,2));
}
sum = add(sum, add(21,21));
for (int i = 0; i < 5; i++) {
sum = add(sum, sub(i,2));
}
}
Lets try to understand what the code is actually doing. The first function obviously calculates the sum of two given integers x and y while the second function is calculating the difference between two given integers x and y. The main function is just a starting point for the actual algorithm that uses the two functions defined before. The algorithm just defines a sum variable that will hold a value which is modified by the following two for loops. The for loops are just invoking the add and sub methods. We do not need to discuss about the intellectual value of this code since it is just some code that can easily be tested against a specification. OK, the C application is ready to use. Time to create a specification for our code…
The files containing TeSSLa specifications are files having the .tessla extension. Such a file is currently missing in our project so create a new file called spec.tessla. Enter the following lines of code for the specification:
define add_event : Events
:= function_calls("add")
define sub_event : Events
:= function_calls("sub")
define add_count := eventCount(add_event)
define sub_count := eventCount(sub_event)
define diff := sub(add_count, sub_count)
define error := geq(diff, literal(2))
out diff
out error
Lets figure out what this specification describes. The first two lines are defining events occurring in the execution of our program. The events we are looking for are function calls as you might guess when you are looking to the right side of the assignment. The first event represents the add function calls and the second event represents the sub function calls. After that we define two variables each of them contains a number representing how often the respective functions were called. Then we just form the difference between both values to get a comparison value. The last line containing a define checks if the difference of both function call counters is greater or equal two. The last two lines defining outputs for the values of diff and error. In other words: the specification says there have to be at least 2 more add calls then sub calls.
The application and the specification are ready… time to check if our program meets the specification. If the TeSSLa-Atom-Package was not already started we will do this now. Go to Packages – TeSSLa – Toggle or hit CMD+Shift+T. If one of the two files we just created is open while activating the package a split view should be set up. On the left side of the split view all C files of the current project should be opened. On the right side all specification files should be opened. Also a toolbar should be appeared on the right side of the workspace. The toolbar contains all buttons we need for testing our example.
The most important button in the toolbar is the forth bottom from top (the circled dot) which will compile the C file from the project into assembly. The assembly then will be modified by linking the libFunctions.so into the assembly code and once this is done the clang makes an executable binary out of the resulting file. The linked libFunctions.so ensures that a log file is generated while executing the binary. The log file is shown in the listing below. The first part of each line contains the type of event that occurred during execution (in this example this events are only function_calls). The event is seperated from the event name by a colon (in this case the name is add which means the add function was invoked).
This log file contains timestamps that belong to certain function call. After that the IDE takes the TeSSLa specification file and hand it on to the compiler which creates an so called AST (Abstrakt Syntrax Tree) from it. On the last stage the log file and the specification AST are passed to the server that is doing an evaluation.
function_calls:sub nil 1493898388 285860
function_calls:add nil 1493898388 286876
function_calls:sub nil 1493898388 287872
function_calls:add nil 1493898388 288916
function_calls:sub nil 1493898388 290417
function_calls:add nil 1493898388 292248
function_calls:sub nil 1493898388 293808
function_calls:add nil 1493898388 295242
function_calls:sub nil 1493898388 296255
function_calls:add nil 1493898388 297214
function_calls:add nil 1493898388 298161
function_calls:add nil 1493898388 299423
function_calls:sub nil 1493898388 300363
function_calls:add nil 1493898388 301694
function_calls:sub nil 1493898388 302523
function_calls:add nil 1493898388 303416
function_calls:sub nil 1493898388 304328
function_calls:add nil 1493898388 305388
function_calls:sub nil 1493898388 306338
function_calls:add nil 1493898388 308604
function_calls:sub nil 1493898388 309627
function_calls:add nil 1493898388 310673
To execute all files in the project including the TeSSLa specification just hit Cmd+T. Some pop-ups showing successful steps are poping up. After the results were printed into console the server has to be stopped since it will stay in idle mode ready to get more input that will not be passed to it. Stop the process by clicking the square button in the tool bar or by hitting Ctrl+C. After stopping the server the the result will be formatted in the lower section of the sidebar.
The toolbar also offers the functionality to compile and/or execute C code without considering the related specification file to make it easier to develop and test the actual application first before trying to run against a specification. So all steps are done that are needed to set up a TeSSLa environment and take it in use. If there are still some questions that were not answered in this tutorial we recommend you to take a closer look on the links that were mentioned at the beginning of this tutorial. The TeSSLa-Atom-Package documentation will describe the GUI and the behavior of the package in detail and the other links may clear up questions about the compiler and other components that are used by the IDE.