Tools

AutoBlackTest

Automatic test case generation is a key ingredient of an efficient and cost-effective software verification process. AutoBlackTest focuses on testing applications that interact with the users through a GUI, and generates test cases at the system level. AutoBlackTest uses reinforcement learning to learn how to interact with the application under test and stimulate its functionalities.

Click here for more information about AutoBlackTest

AVA

Automata Violations Analyzer, AVA, is a technique to automatically produce candidate interpretations of software failures from anomalies identified by anomaly detection techniques. Interpretations capture the rationale of the differences between legal and failing executions with user understandable patterns that simplify identification of failure causes. Empirical validation conducted both with synthetic cases and third-party systems showed that AVA produces useful interpretations.

Click here for more information about AVA

BCT

BCT is a tool that automatically identifies anomalous events that likely caused failures, filters the possible false positives, and presents the resulting data by building views that show chains of cause-effect relations, i.e., views that show when anomalous events are caused by other anomalous events. BCT comes with a library that provides its core functionality and an Eclipse plugin that provides management and visualization facilities.

Click here for more information about BCT

GASP

GASP (Genetic And Symbolic Performance analyzer) is a tool that performs a WCET (Worst-Case Execution Time) analysis of Java programs, aimed at producing a test case that maximizes the execution time of the program under analysis. To this end, it exploits symbolic execution and memetic search on the space of possible path conditions.

Click here for more information about GASP

JBSE

JBSE (the Java Bytecode Symbolic Executor) is a special-purpose Java virtual machine for the analysis of software. JBSE performs a very precise kind of analysis called symbolic execution, based on the actual simulation of the program according to the Java Virtual Machine specification v.8. JBSE can be applied for assertion-based verification of software compiled to Java bytecode, and is used in our SUSHI, TARDIS and GASP tools.

Click here for more information about JBSE

KLFA

KLFA is a tool that automatically analyzes log files and retrieves important information to identify failure causes. KLFA automatically identifies dependencies between events and values in logs corresponding to legal executions, generates models of legal behaviors and compares log files collected during failing executions with the generated models to detect anomalous event sequences that are presented to users.

Click here for more information about KLFA

LINK

Link is a technique to automatically generate test cases for GUI-based applications that process complex data, such as maps, personal data, book information, travel data. The novel idea of Link is to exploit the Web of Data to generate test data that match the semantics of the related fields, and satisfy the semantic constraints that arise among interrelated fields. Link automatically analyzes the GUI of the application under test, queries Linked Data KBs to extract the data that can be used in the tests, and uses the extracted data to generate complex system test inputs.

The tool will be available soon. Please contact santoro@disco.unimib.it if you want to receive a notification email when the tool will be on-line.

MASH

The majority of IDEs implement a concept of plug-in that nicely supports the integration of tools within the IDEs. Plug-ins dramatically simplify the structural integration of multiple tools, but provide little support to the design of the dynamic of the integration, which must be entirely coded by programmers from plug-ins’ API. Manually integrating plug-ins is costly, complex and requires a deep understanding of the underlying environment. The implementation of tools as plug-ins and the integration of the results produced by different plug-ins are still difficult, expensive and error-prone activities. In our vision, IDE users must be able to execute plug-ins and integrate their results by designing workflows that can be persisted, executed and re-used in other workflows. MASH is an Eclipse plug-in that enable users to compose the functionality provided by different plug-ins at runtime, by drawing a workflow in their workspace.

Click here for more information about MASH

RADAR

RADAR (Regression Analysis with Diff And Recording) is a technique for debugging regression faults. RADAR combines monitoring, model inference and anomaly detection into a solution for the automatic identification of the anomalous behaviors that caused a regression failure. RADAR is implemented as an Eclipse plug-in and allows developers to analyze failures directly in the Eclipse IDE. In particular, RADAR can visualize the chain of anomalous behaviors that caused a failure, and provide developers a rich set of dynamic data that can be used to understand the context of the failure.

Future versions of RADAR will leverage Grammatech CodeSurfer static analysis capabilities to precisely pinpoint the code changes that lead to the regression.

Click here for more information about RADAR

SUSHI

SUSHI (Symbolic Unit testing via Search of Heap Inputs) is an automatic test case generator for Java programs, aimed at achieving high branch coverage. It leverages symbolic execution to calculate, from a program path that reaches a branch, a path constraint, i.e., a constraint on the program inputs that, when satisfied, allows to cover the path. SUSHI calculates path constraints by exploiting the symbolic executor JBSE. To solve path constraints SUSHI transforms them in search problems and feeds by them the search-based test case generator EvoSuite.

Click here for more information about SUSHI

TARDIS

TARDIS (meTAheuRistically-driven DynamIc Symbolic execution) is an automatic test case generator for Java programs, aimed at achieving high branch coverage. It leverages a technique called dynamic symbolic (a.k.a. “concolic”) execution, to alternate symbolic execution performed with the symbolic executor JBSE, with test case generation, performed by finding solutions to symbolic execution path constraints with the test case generator EvoSuite.

Click here for more information about TARDIS