Present Projects

MoMuT (Model-based mutation testing)

MoMuT is a tool we develop at AIT, that generates test-cases from a model. The model can be an UML behavioural model with a state machine (though Event-B is also supported). A large number of mutated models are generated internally, whereas a mutation is a small change in the model. The tool then proceeds to generate test-cases that are able to distinguish the mutated models from the original, thereby providing mutation coverage. These test case can be run against an implementation. This gives the customer the ability to generate test from the specification (model) before even starting to implement.

ThreatGet

ThreatGet is a cybersecurity threat analysis tool. It analyses customer-created architecture models of critical systems, such as from the automotive or IoT domain. Additionally, AIT provides a meta-model and a threat model. The meta-model is a set of elements and attributes that can be used in the architecture model. The threat model is a set of rules in a domain specific language with a formally defined semantics. The tool generates a report of threats detected in the architecture model.

Past Projects

Liss (Language Inclusion-based Synchronisation Synthesis)

Liss is the implementation that accompanies our paper [1]. It is a synthesis tool that is given a concurrent C program and will insert synchronisation primitives until the behaviour of the concurrent version of the program is identical to the sequential version. It is currently a research prototype.
GitHub

Limi (Language Inclusion Modulo Independence)

Limi (Language Inclusion Modulo Independence) is a template library that implements the basic antichain algorithm [2] modulo an independence relation. The library takes as input two non-deterministic finite automata A and B with a shared alphabet and an independence relation I over the symbols of the alphabet. The independence relation determines for two symbols if they are independent. Two strings of the language are equivalent module independence if they are identical up to swapping independent symbols. The formal definition is given in our paper [1].
GitHub

The usage of the library is explained in detail on the project page.

TARA

TARA is the implementation that accompanies our paper [3]. The tool accepts concurrent traces in a custom language and returns a succinct error explanation in the form of a DNF over happens-before relations. This can be used for synthesis or fault localisation.
GitHub

[1] Pavol Černý, Edmund C. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis. In CAV 2015

[2] Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin. Antichains: A New Algorithm for Checking Universality of Finite Automata. In CAV 2006

[3] Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, Thorsten Tarrach. Succinct Representation of Concurrent Trace Sets. In POPL 2015