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.
The ABS core tools consist of
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.
To check an ABS model (a set of ABS files) for syntax and type-errors, run
java -jar absfrontend.jar <absfiles>
Java code generation is done by the ABS Java backend.
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.
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.
The Maude backend is responsible for generating Maude code from ABS models. Maude is a tool for executing models defined in rewriting logic.
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.
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.
Products defined in a product selection are validated with respect to a given feature model using the mTVL tools, which are provided by the absfrontend.jar file.
Products are validated with respect to a given feature model using the ABS tools. For example, the following command verifies that the product HighEnd satisifies the feature model (both feature model and product are defined in the ChatPL.abs file).
java -cp absfrontend.jar abs.frontend.parser.Main -check=HighEnd ChatPL.abs
Flattening an ABS model means applying a sequence of deltas to a core ABS model, in order to obtain the behaviour of a particular product. In the ABS compiler front end, the -product=name switch triggers the flattening for the given product. For example:
java -jar absfrontend.jar -product=P1 HelloWorld.abs
The flattening process is performed at the level of the AST, which is subsequently used to generate Java code.
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.
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.
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.
Just go to the web interface tab at the COSTABS web site and follow the steps there provided.
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:
For more details on the meaning of the COSTABS parameters go to chapter 3 of deliverable 4.2.
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 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.
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