The Erlang simulator is the main tool for simulating and visualizing all aspects of an ABS model, including resource usage and deployment configuration. It relies on the common compiler frontend and type checker, and generates code in the Erlang language which is subsequently compiled and run on the Erlang BEAM VM. The Erlang simulator comprises a compiler backend to generate Erlang code, compile it and generate an OTP-compliant Erlang application. Included is the embedded cowboy web server, which enables data access to a running model. This is used for implementing visualization and the Model API, including inspection of objects and deployment components and invoking ABS methods from outside the model.
2 Deadlock Analysis (SACO)
In general, deadlock situations are produced when a concurrent program reaches a state in which one or more tasks are waiting for each other termination and none of them can make any progress. In ABS, the combination of non-blocking and blocking mechanisms to access futures may give rise to complex deadlock situations and an analysis is required to ensure deadlock freedom. This tool, which is available in the Envisage collaboratory, provides a framework that allow us to verify if our programs have deadlocks. It also returns hints to help users to identify the cause of the deadlock found.
3 Deadlock Analysis (DSA)
The Deadlock Static Analyser (DSA) performs a static and sound deadlock analysis of ABS programs. Deadlocks may be particularly hard to detect in systems with unbounded recursion and dynamic resource creation, such as server applications, which creates an unbounded number of processes.
In order to augment precision and scalability we propose a modular framework combining several techniques. We meet the scalability requirement by designing a front-end inference system that automatically extracts abstract behavioral descriptions pertinent to deadlock analysis, called behavioural types, from code. The inference system is modular because it (partially) supports separate inference of modules. The inference system mostly collects method behaviors and uses constraints to enforce consistencies among behaviors. Then a standard semiunification technique is used for solving the set of generated constraints.
The tool returns if the program analyzed is deadlock free, the current release of the tool and the time for performing the analysis.
4 Systematic Testing (SYCO)
SYCO is a systematic tester for ABS concurrent objects. The user interacts with SYCO through its web interface which is integrated within the ABS collaboratory. The SYCO engine receives an ABS program and a selection of parameters. The ABScompiler compiles the program into an abstract-syntax-tree (AST) which is then transformed into the SYCO intermediate representation (IR). The partial order reduction (DPOR) engine carries out the actual systematic testing process. The output manager then generates the output in the format which is required by EasyInterface, including an XML file containing all the EasyInterface commands and actions and SVG diagrams. In case deadlock-guided testing is applied, the DECO deadlock analyzer is invoked, which returns a set of potential deadlock cycles that are then fed to the DPOR engine to guide the testing process (discarding non-deadlock executions).
5 Test Case Generation (aPET)
aPET is a static testing tool and test case generator for ABS concurrent objects based on symbolic execution. In symbolic execution the program execution is simulated for possibly unknown inputs hence using symbolic expressions for program variables. As a result, it produces a system of constraints over the inputs containing the conditions to execute the different paths and the expressions computed for their outputs. Symbolic execution has many applications, namely software verification, program comprehension and automatic test case generation (TCG). In this latter context, symbolic execution produces, by construction, a (possibly infinite) set of test cases, which satisfy the path-coverage criterion.
The usage of aPET is essentially as follows: given an input program and a selection of methods, the aPET symbolic execution engine computes a set of test cases for the selected methods. Test cases can be given as path constraints or, after a constraint solving procedure, as concrete test cases.
6 Resource Analysis (SACO)
SACO is a Static Analyzer for Concurrent Objects which is able to infer deadlock, termination and resource boundedness of an ABS program.
SACO can measure different types of costs. The user can select among the following cost metrics: termination (only termination is proved), steps (counts the number of executed instructions), objects (counts the number of executed newinstructions), tasks (counts the number of asynchronous calls to methods), memory (measures the size of the created data structures), data transmitted (measures the amount of data transmitted among the distributed objects), user-defined model (allows to write annotations in the code of the form [cost == expr] and the analysis accumulates the cost specified by the user in expr every time this program point is visited).
In the output, it returns upper bounds on the worst-case cost of executing the concurrent program. The results of our termination analysis provide useful information for cost: if the program is terminating then the size of all data is bounded. Thus, we can give cost bounds in terms of the maximum and/or minimum values that the involved data can reach.
7 Resource Analysis (SRA)
SRA computes upper bounds of virtual machine usages in a dialect of ABS, called vml, with explicit acquire and release operations of virtual machines. In this language it is possible to delegate other (ad-hoc or third party) concurrent code to release virtual machines (by passing them as arguments of invocations). Our technique is modular and consists of (i) a type system associating programs with behavioural types that records relevant information for resource usage (creations, releases, and concurrent operations), (ii) a translation function that takes behavioural types and return cost equations. It is integrated with the solver CoFloCo that given the cost equations produces the result.
It returns a set of tabs containing the behavioural types generated, the cost equations and the upper bounds inferred.
8 Smart Deployer
The key idea of SmartDepl is to allow declarative specifications what the user wants to deploy, and develop the program abstracting from concrete deployment decisions. More concretely, the user specifies her deployment requirements as program annotations. SmartDepl processes them and generates for every annotation a new class that specifies the deployment steps to reach the desired target. The user can use this class to trigger the execution of the deployment, and to undo it in case the system needs to downscale.
9 Code Generation (Haskell)
The tool translates ABS code to Haskell and subsequently to native code, which is then linked to our custom-developed Haskell library to provide the concurrency of an ABS runtime. Compared to other back-ends (Erlang, Maude) the Haskell back-end relies on an external Haskell type-checker and Garbage Collector. Besides the standard ABS language, the tool implements the Cloud extension, for real deployment and distributed execution of ABS models in the Cloud, as well as the HTTP-API extension, for interacting with running ABS code from the outside. The Haskell back-end is open-source and utilizes BNFC, a Haskell parser generator, later also adopted by the Java back-end.
KeY-ABS is an interactive (semi-automatic) deductive verification tool that enables one to verify functional correctness properties for concurrent and distributed ABS models. The specification is provided in term of history-based class invariants. It is then proven that the ABS model adheres to its specification. The approach is symbolic and models the ABS language faithfully, i.e., it does not apply any abstraction and remains fully precise. The specification language is first-order (dynamic) logic and thus highly expressible. KeY-ABS is an open source software written in Java. It is a variant of the KeY verification system for Java. As input it requires the ABS model to be verified as well as its specification, or alternatively, a problem file with the formula to be proven. The specification is provided as separate files located in the same directory as the ABS files. The user can then start the verification for each method separately. The proof-obligation to be proven is then loaded into the theorem prover of KeY-ABS. The verification process is semi-automated, i.e., KeY-ABS provides powerful strategies for automation but requires sometimes user interaction.
11 Monitoring of SLA Metrics
The are several tools related to monitoring such as SAGA,METVIZ or LOGREPLAY.
SAGA is a tool that generates executable ABS monitoring add-ons for SLA, SLO and KPI metrics. The approach is event-based: the events are interactions with endpoints from Service APIs (a common example is a call or return of a resource method in a MODEL API). A service metric function is formalized as an attribute from a declarative attribute grammar, which maps an event traces to a value that indicates the QoS level. SAGA requires two inputs: a communication view that names the events relevant for the metric to be formalized, and an attribute grammar where the value of the metric is defined. SAGA then fully automatically generates ABS code for a parser (an automaton) corresponding to the grammar. An Eclipse-based syntax highlighting module for views and grammars is available. SAGA is implemented as a meta-program in the language Rascal.
METVIZ is a tool that relays metrics (as time-series) from an HTTP endpoint in an ABS model to InfluxDB for visualization. LOGREPLAY is a tool to replay a log file as a series of queries onto an HTTP endpoint.
More information is available in the following links.