Model-Based Testing in Java using BIP

The main goal of this project is to provide a mechanism for automated testing of the conformance between BIP specifications and the corresponding Java components.

Context

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.

Project goals

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.

Benefits

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.

Required skills

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.

Location

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

Contact and application

For additional information and to apply please send me an e-mail (in English or French) with the subject “Model-Based Testing internship”.

References

  1. Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, Joseph Sifakis: Rigorous component-based system design using the BIP framework. IEEE Software 28(3) (2011) pp. 41–48 [PDF]
  2. Simon Bliudze and Joseph Sifakis. The Algebra of Connectors — Structuring interaction in BIP. In Proceedings of the 7th ACM & IEEE International Conference on Embedded Software, EMSOFT 2007, pp. 11–20, Salzburg, Austria, October 2007. ACM SigBED. [PDF]
  3. Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, and Alina Zolotukhina. Exogenous coordination of concurrent software components with JavaBIP. Software: Practice and Experience, 47(11):1801–1836, November 2017. [PDF]

Leave a Reply

Your email address will not be published. Required fields are marked *