Model-Based Testing in Java using BIP

BIP [1, 2] is a framework for component-based design of correct-by-construction software and embedded systems. Components are modelled as finite state machines (FSM). In order to provide an abstraction level that would allow reasoning about the parallel behaviour of concurrent components, only the relevant actions are explicitly represented by transitions of these state machines. Interaction and priority models, collectively called glue, are the two mechanisms provided by BIP for the coordination of the concurrent behaviour of the system to enforce desired properties (e.g. "the system reset is only triggered if a detected failure is not followed by a corrective action within a given timespan").

JavaBIP [3] is a Java-based implementation of BIP, initially developed at EPFL. This implementation relies on the so-called BIP Specification classes that are associated to software components to provide an FSM representation of their relevant behaviour. Essentially, BIP Specifications represent an extended interface for such components, which provides information on when operations can be performed, extending the usual notion of interface, which only specifies what operations exist. Availability of such specifications enables the application of the BIP coordination mechanisms. However, their correctness relies exclusively on the expert knowledge of the designer providing the specification.

The main goal of the project is to provide a mechanism for automated testing of the conformance between BIP specifications and the corresponding Java components. The first step of the project consists in creating tests that cover possible execution paths for a component as defined by the corresponding BIP Specification. These tests ensure that component implementation is consistent with the BIP Specification. You will create a fluent API for manual specification of the test cases with assertions to be checked by the tool. The test specification should make it possible to specify the transitions being taken, the data transfers provided, as well as assertions of what guards are enabled/disabled. The second step takes the analysis further, by considering hierarchical classes, where subclasses have FSM defined by BIP Specifications and, potentially, BIP glue imposing coordination constraints on the joint operation of these sub-classes. The tool must allow testing that the the operations performed by an instance of the compound class on the instances of the sub-classes, respect these FSMs and glue constraints.

You will learn the principles of rigorous system design based on formal operational semantics and get an in-depth understanding of BIP, a state-of-the-art component-based framework. Successful internship can lead to a research publication.

Good analytical skills will definitely be required. The candidate must have good understanding of Labelled Transition Systems and Finite State Automata. The work will be done in Java so proficiency in Java is a must. You should be familiar with one of the development environments: Eclipse or IntelliJ.

The internship will be carried out in the Spirals project team at Inria Lille – Nord Europe under supervision by Simon Bliudze.