Software Model Checking in the Multicore Era

contact: ahmed rezine

ceniit project 12.04

Bachelor and master's project proposals

Automatic Detection of Static Problem Bounds for Object Instantiations of UML Class Diagrams

(Bachelor's level, in collaboration with Saab, possibility of economical compensation) Models are often used during the successive design steps of new programs. This allows to describe, explore and reason about different solutions to the problems the new program is supposed to solve. Ensuring consistency and correctness of such models can save important resources by catching errors and problems as early as possible during the design. Indeed, lurking bugs can require important resources to eradicate if noticed at the implementation level. Such costs can be dramatic for safety critical applications. This project deals with such applications at Saab. The goal is to implement a tool, preferably as an Eclipse plugin, to generate static bounds for the number of instances of each class of some specific class diagram description. The class diagram is given in some format together with additional invariants supplied by the user, e.g., in OCL (Object Constraint Language). The student should:

Qualification

This 16 hp thesis will be carried by one bachelor student.

Automatic Detection of Critical Sequences in Safety Critical Reactive Systems

(Master's level, in collaboration with Saab, possibility of economical compensation) The behavior of many computer systems is not captured, in a satisfactory manner, in terms of some input/output function. Instead, such systems are meant to continuously run and to react to their surrounding, be it the user, the environment, or both. Some reactive systems are safety, i.e., any error or misconception in their executions can have dramatic consequences. One cannot afford to just restart the system. It is therefore important to analyze the behavior of such systems in order to make sure that certain properties do hold under all executions. If some property does not hold, it is then important to exhibit concrete executions illustrating this fact. This project focuses on automatizing the analysis of specific reactive systems given in terms of finite state machines sharing among themselves and with their surrounding a number of (internal) queues and variables. The objective of the project is to ensure that certain bounds on the possible executions are always respected for environments following certain patterns, or to exhibit concrete counter-examples. For this purpose, different techniques are to be discussed and a tool is to be implemented in order to:

Qualification

This 30 hp thesis will be carried by one Masters student.

Incremental Inductive Verification, Does It Work? Does It Scale?

(Master's level, relevant for Prover Technology) Modern Multicore Computers are able to deliver a greater computing power for programs that can be run in parallel. This generated a great amount of work in coming up with ways to run programs in parallel. This project explores using Multicores to perform verification tasks. As opposed to testing and simulation, verification aims at exploring all possible scenarios before validating a program or a design. Verification typically targets safety critical systems (transportation, medical instruments, etc). The price of the supplied guaranty is a complexity that often limits verification efforts to only target (relatively) small and simple computer systems. An important amount of work aims at coming up with clever verification techniques and algorithms that allow to handle larger and more complex systems. Among the newly developed algorithms for the verification of computer systems, some are particularly well suited for performing parallel verification. This project will experiment possibilities of running them on a multicore platform.

Qualifications

This 30 hp thesis can be carried by one or two Masters students that:

Verification of Synchronization patterns of GPU programs

(Master's level) More and more programs involve pieces of code targeting GPU platforms. This is particularity true for programs that allow for highly parallel computations. The problem is that the sought after gain is only achieved with low level tuning at threads level. This entails a degree of intricacy that make writing such programs extremely error prone and difficult to get right. Testing and simulation based debugging are typically difficult in this context due to the concurrent and intricate nature of these programs. Promissing verification techniques already exist. This project is part of an effort that aims at verifying the absence of certain synchronization errors. For this, GPU programs need to be parsed and relevant synchronization parts need to be isolated. This project aims at isolating the synchronization patterns in typical GPU programs.

Qualifications

This 30 hp thesis can be carried by one or two Masters students that:

Systematically checking concurrent code

(Master's level) Powerful Multicore computers are now widespread and more and more concurrent code is being produced in order to get the most of these platforms. The problem is that designing, implementing, testing and debugging concurrent programs can be much more challenging and intricate than for sequential ones. Typically, concurrent programs allow for a huge number of possible interleavings between their concurrent sequential parts. Many bugs only appear in a fraction of these possible interleavings. Traditional testing approaches would only explore a tiny portion of these interleavings, leading to embarrassing hidden bugs mysteriously appearing at the customer site. The student(s) will start by gaining familiarity with a number of tools (with available source code) for the systematic testing of concurrent programs. An important part of the work will then be to collect a set of benchmarks of concurrent code, either from existing work, from open source applications, or from Ericsson applications. It is expected that an important part of the code will be in a language different from the one handled by the targeted tools. The benchmarks might therefore have to be rewritten to C# and Java. The thesis will leverage on the availability of the source code in order to modify the tools and to experiment with different heuristics, combining with user supplied hints or with other verification or static analysis techniques.

Requirements

This 30 hp thesis can be carried by one or two Masters students that: