The ABS Tool Suite

This site contains information about the ABS tools suite. The Abstract Behavioral Specification Language (ABS) is a concurrent object-oriented modeling language that features functional data-types. The current language specification is available as a PDF file.

Core Tools

The ABS core tools consist of

  1. A parser and syntax-checker
  2. A type-checker and semantic analyser
  3. A Java code generator
  4. A Maude code generator

The ABS core tools are all contained in the absfrontend.jar JAR file. The tools should be executable on all systems with an installed Java Runtime Environment (JRE). The minimal required version is JRE 1.6.

Syntax- and Type-Checking

To check an ABS model (a set of ABS files) for syntax and type-errors, run

java -jar absfrontend.jar <absfiles>

Java Code Generation and Execution

Java code generation is done by the ABS Java backend.

Java Code Generation

To generate Java code from an ABS model, run

java -cp absfrontend abs.backend.java.JavaBackend -d <targetdir> <absfiles>

If the command is successful it will generate Java source and JVM class files into the <targetdir> directory.

Executing Generated Java Code

The Java backend generates for every Main block that exists in an ABS model, a corresponding Main class that contains a standard Java main method. Thus, the generated Java code can be executed like any other standard Java code by using the java command. The generated Java code relies on a runtime library (included in the absfrontend.jar), which must be provided when executing the system. To execute the code generated can use the following command on the command line:

java -cp <targetdir>:absfrontend.jar <MainModule>.Main

where <targetdir> is the directory that contains the generated Java classes and <MainModule> is the name of the module that contains the main block.

Maude Code Generation and Execution

The Maude backend is responsible for generating Maude code from ABS models. Maude is a tool for executing models defined in rewriting logic.

Maude Code Generation

To generate Maude code run

java -cp absfrontend.jar abs.backend.maude.MaudeCompiler <absfiles> -o <outputfile>.maude

This will generate a file Maude file <outputfile>.maude.

Maude Execution

To execute the generated Maude file, load the file into Maude. When loading, Maude expects the file abs-interpreter.maude to be either already loaded, in the same directory as the generated file or in a directory included in the environment variable MAUDE_LIB. The model's main block is started by the following command:

rew start .

The result of evaluating is a dump of the complete system state of the model, with one Maude term for each class, cog, object, and future variable.

Product Selection and Validation

Product selections are validated with respect to a given feature model using the mTVL tools. These tools are provided by the mtvl.jar file. Note that this JAR file depends on the absfrontend.jar file. To execute the mTVL tools use

java -jar mtvl.jar

make sure in that case that the absfrontend.jar file is located in the same directory as the mtvl.jar file.

Integrated Development Environment

ABS features an Integrated Development Environment (IDE) for writing ABS models. The IDE is realized as an Eclipse plug-in for the current Eclipse distribution version 3.6 (Helios). It can be installed by using the standard Eclipse installation routine via the update site http://tools.hats-project.eu/update-site.

More information

COSTABS

COSTABS is a research prototype which performs automatic program analysis and which is able to infer cost and termination information about ABS programs. The system receives as input an ABS program and a cost model chosen from a selection of resource descriptions and tries to bound the resource consumption of the program with respect to the cost model. COSTABS provides several notions of resource: number of instructions, size of functional data, number of concurrent objects and number of spawned tasks.

When performing cost analysis, COSTABS produces a cost equation system, which is an extended form of recurrence relations. In order to obtain a closed (i.e., non-recursive) form for such recurrence relations which represents an upper bound, COSTABS includes a dedicated solver called PUBS (more information here). An interesting feature of COSTABS is that it uses pretty much the same machinery for inferring upper bounds on cost as for proving termination (which also implies the boundedness of any resource consumption). See chapter 3 of deliverable 4.2

COSTABS has three different interfaces: a command-line interface, a web interface and an Eclipse plugin. The command-line interface allows using COSTABS as a standalone application, which provides a layer from which more advanced interfaces can be easily built. The web interface allows users to try out the system, without installing it. In addition, it provides a set of representative examples of ABS programs, and allows users to upload their own ABS programs. The most advanced (and highly recommended) interface is the Eclipse plugin, which is fully integrated into the main ABS tool suite, and thus allows the programmer to use COSTABS during the development process of ABS applications.

Installation and usage instructions

Command-line interface

The COSTABS command-line tool can be downloaded from the (Download tab at the) COSTABS web site (currently only available for Linux systems). Detailed instructions on how to install and use it are available in the README file which is downloaded. Typing the command costabs -h displays some usage information.

Web interface

Just go to the web interface tab at the COSTABS web site and follow the steps there provided.

The Eclipse plugin

The COSTABS Eclipse plugin is completely integrated into the ABS tool suite. It is therefore installed by default when installing the ABS tool suite (follow the instructions here).

In order the use the COSTABS Eclipse plugin follow these instructions:

  • First, the functions and/or methods to be analyzed must be selected in the outline view (assuming and ABS source file is opened). To select multiple functions and/or methods keep pressed the control and/or the Caps key.
  • To invoke COSTABS we click on the palm-tree button in the tool bar (or alternatively select the option Analyze with Costa from the Costa menu). We now see the COSTABS preferences window where we can set the parameters of COSTABS (see below for details).
  • Once the parameters have been set we click the Analyze button. This will launch the actual analysis. The results of the analysis are displayed in the Eclipse COSTABS console window (at the bottom). Additionally, the interface produces square markers associated to the analyzed methods/functions in the source file. Moving the mouse over such markers we can see a pop-up window where the corresponding upper-bound is displayed.

COSTABS parameters

  • Cost model: Briefly, a cost model is a function that maps each instruction to the amount of resources consumed when executing it. COSTABS provides the following cost models: termination, steps, memory, objects and task-level.
  • Cost centers: Enabling this feature COSTABS will obtain the cost per component (also called cost-centers) rather than a single cost expression. The current implementation of COSTABS assumes that objects of the same type belong to the same cost center, i.e., they share the processor.
  • Size norm: When a program manipulates numerical data, its cost often depends on the initial (integer) values of the corresponding variables. However, when it manipulates terms (i.e., data-structures), its cost usually depends on the sizes of the inputs. A size norm is a function that maps terms to numerical values that represent their sizes. The following size norms are available in COSTABS: term-size, which corresponds to the number of type constructors in a given term, and, term-depth, which corresponds to the length of the longest path in the term.
  • Debugging mode: The debugging mode produces on-screen detailed information of the different phases and generates files with some useful intermediate information such as the rule-based representation (an intermediate representation for ABS programs) and the cost-relation system.
  • Asymptotic bounds: Enabling this feature COSTABS obtains asymptotic upper-bounds rather than concrete upper-bounds.
  • Verbosity: COSTABS allows setting three verbosity levels, named 0 (the least verbose) to 2 (the most verbose).

For more details on the meaning of the COSTABS parameters go to chapter 3 of deliverable 4.2.

Helping the analyzer with class invariants

COSTABS provides a way to incorporate class invariants on the analyzed ABS code. Those invariants can provide, e.g., guarantees on the global states when the process is resumed after an await statement. Annotations can be written right before await statements or right before method definitions (currently those are the only places where they can be needed). The are written in ABS format, each annotation between []'s, with the special functions 'old', 'max' and 'min'. See the annotations in the ABS examples at the COSTABS web site.

For example, if we add the following invariant

[old(f) == f][f <= max(f)][f > 0]

right before an await instruction then we state that it is guaranteed that when the process resumes, the value of field f will be the same as when the process was suspended, and also that f is bounded by var max(f) and it is always positive. This kind of invariants are sometimes needed in order for the analyzer to bound the number of iterations on loops.

See more details on chapter 3 of deliverable 4.2

Note: In the previous version of COSTABS invariants were written in a pseudo-JML format. E.g., the one above was written

//@invariant \old(f) == f

This syntax is not valid anymore since we are now adhering to the ABS annotations format.

JMS2ABS: Automated Extraction of ABS Models from JMS Applications

JMS2ABS is a research prototype tool that automatically extracts ABS models from JMS programs in bytecode form. In the zipped file you will find an executable binary named jms2abs, prepared to run on 32-bit Linux systems, a README file with usage instructions and contact information for support, and two directories: sources and examples.

Dependency Management

ABS is supported by Maven dependency management system.

Maven is based on the concept of a project object model (POM), Maven can manage a project's build, reporting and documentation from a central piece of information.

Maven support for ABS features a abs-maven-plugin that provides functionality to

  • compile, generate backend codes from ABS models
  • execute test cases written in ABS
  • package ABS models into standard ABS packages (APK)
  • deploy ABS packages as reusable artifacts into a global repository

More information