Validation of inter-process communication in an Océ copier

title:Validation of inter-process communication in an Océ copier
company:Océ, TNO-ESI
keywords:verification, modeling, process communication
topics:Case studies and Applications
contact:prof.dr. J.C. van de Pol & Jacques Verriet (Océ) & G.J. Tretmans
to be started:as soon as possible

External Master Assignment


Department Description:

TNO-ESI is a leading research group for high-tech embedded systems design and engineering. It has a close cooperation with high-tech industry, as well as a strong association with fundamental research of academia, both national and international. TNO-ESI contributes to society and economy by driving advances in high-tech systems technology, with a strong shared research programme, dedicated innovation support, a focused competence development programme, and various knowledge-sharing activities.

Océ, a Canon Group company, is an international leader in digital document management and printing for professionals. Many Fortune 500 companies and leading commercial printers use Océ solutions for wide format printing, high-speed production printing and document-related business services. Océ employs 4,000 specialists at innovation and technology centres in Europe, North America and Asia. Through its own Research & Development (R&D) Océ develops core technologies and the majority of its own product concepts.


Context Description:

In some of its products, Océ uses an own developed inter-process communication framework. This framework allows applications developed in different programming languages (e.g. C++, C#, Java) to communicate with each other. This framework is used intensively and its usage is expanding. The quality of this critical component is to be guaranteed for future developments and changing environments. Therefore we would like to create models of the framework and use these to formally analyse the correctness and robustness of its highly parallel implementation. Aspects we would like to see evaluated include correctness, reliability and robustness, freedom of deadlocks, and scalability. Implementation aspects to consider include unpredictable external events (e.g. connection losses), multi-threading, and memory management.


Assignment description:

This assignment involves the validation of the inter-process communication framework developed by Océ. Traditional validation involves extensive automated and manual testing. With this assignment, you will evaluate formal validation techniques, such as model checking (using tools such as Uppaal, Dezyne, or mCRL2) and model-based testing (using tools such as TorXakis, JTorX, or SpecExplorer), for system validation. The formal techniques are to be compared to the traditional testing-based validation approach with respect to their effectiveness, efficiency, and usability.