Motivation

In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the following:

• The state of the art of software model checking techniques is substantially more advanced than deductive techniques. More interesting and complex properties can be automatically proved than with deductive methods. Consequently these methods are much more used in industry than deductive methods.

• The above does not mean that deductive methods are doomed to be abandoned: on one hand the soundness and completeness of these methods (with no false errors), as well as the expressiveness of the logical languages used and the general flexibility of their application make them highly desirable (especially in the critical context); on the other hand it is expected that, as was previously the case for sequential code, automation levels will increase and render such methods more usable.

The current project has the double purpose of advancing the state of the art and providing results that can be brought to practice in the very short term by our industrial partners. Since software model checking techniques are currently much more advanced and usable in practice than deductive methods, one task of the project will be dedicated to producing a practical verification platform suited to specific needs and programming languages. On the other hand, the deduction-based approach to verification of concurrent software has become an exciting area, in which the team wants to contribute with fundamental research.

Our approach will be guided by three simples principles, as follows:

1. It will be incremental, starting from languages with restricted data structures and models for concurrency. This is particularly adequate for critical software, since in this area the programming languages that are used are often subject to restricted profiles that forbid less predictable behaviour.
2. It will combine path sensitive and path insensitive techniques, and exploit their interaction. It is our firm belief that the key to successful automatic verification lies in this combined approach.
3. All the methods and tools produced will be validated through real-life use cases, provided and carried out by team members who work directly in the development of embedded critical software.

We now detail our plan and the reasons why we think these three principles will lead us to successful solutions.

I.

Since C and Ada are the languages of choice in the development of embedded critical systems, we will start by addressing the verification of concurrent programs of subsets of both languages. In the case of Ada, the choice goes naturally to the RavenSPARK language, which has the enormous advantage of being a commercially successful product, widely used in industry, and having ideal characteristics for our purposes: a restricted model of concurrency; restricted data structures (no aliasing is possible); an annotation language comprising assertional and dataflow contracts; and the availability of a toolset for checking both dataflow and assertions. Furthermore the team possesses experience in the verification of sequential SPARK code. The presence of dataflow annotations, complemented by a model of concurrency that forbids the dynamic creation of threads, can be taken into account to calculate predicate abstractions of concurrent programs, since the amount of interference between threads is naturally limited by the dataflow restrictions, which can be taken for granted since they can be effectively checked by the SPARK toolset. Also, rely and guarantee conditions are intrinsically related to dataflow annotations of individual threads of a program. It will be interesting for instance to see if such conditions can be automatically inferred from the compulsory dataflow annotations that must be present in every valid RavenSPARK program.

II.

Approaches to program verification that combine different techniques are seen as promising, even if it may be difficult for a team to acquire the required know-how. We intend precisely to take advantage of the fact that know-how is in place, as a result of a process carried out over the past 5 years in a number of projects, collaborations, and doctoral theses. Predicate abstraction, which is a fundamental component of any software model checking system, is typically implemented with the help of a weakest precondition algorithm -- a deductive technique. In this project we will be in a position of deep understanding of the deductive aspects of verification, which may allow us to produce predicate abstraction algorithms tailored to our needs. Moreover, since the study of predicate abstractions for concurrent programs is a practically untouched field, it may well be the case that the rely-guarantee principles and verification conditions algorithms can be used fruitfully for predicate abstraction (some published work hints at this).

Finally, it is our conviction that a mixture of software model checking and deductive verification can be in itself a very powerful verification method. Rely-guarantee reasoning is based on two separate aspects: "intra-thread" verification conditions for each thread (taking as assumptions rely and guarantee conditions of all the threads in the program), and "inter-thread" verification conditions, to assert (compositionally) that if all threads satisfy a given property then the ensemble does so as well. We will investigate the possibility of each of these aspects being verified by different methods; we will for instance use a SMC to check intra-thread properties and rely-guarantee reasoning for the compositional aspect. This may still result in an acceptable level of automation in the proofs. In the other direction we will also investigate the use of predicate abstraction itself as a tool for deductive verification at the inter-thread level, since rely-guarantee VCs may be easier to establish for over-approximated code.

III.

This project stems from an ongoing collaboration between academics and practitioners. The team brings together

• Specialists in verification from CCTC and CMAT, Univ Minho, and LIACC, Univ Porto, who will work on the theoretical aspects of all the main tasks of the project: predicate abstraction (CCTC and LIACC, task 1); properties of models (LIACC, task 2); and deductive techniques (CMAT, CCTC, and LIACC, task 3).
• Researchers who are expert in embedded, safety-critical, and real-time concurrent programming, from CISTER, IPP, will work on the development of the SMC platform (task 2), provide use cases, and carry on an evaluation of the tools and methods obtained as outcomes of the project (task 4).

Main Results

The main results of the project will include (for at least one of the programming languages of interest in the safety-critical context)

• a novel predicate abstraction algorithm and the corresponding implementation
• a SMC toolkit for concurrent applications
• a prototype generic SMC toolkit (multi-language, multi-checker)
• a VCGen for rely-guarantee conditions
• a general method for verification of concurrent programs combining both path-sensitive and path-insensitive techniques.

Main novelties include (i) taking advantage of specific aspects of relatively simple programming languages used in safety-critical development, and (ii) combining techniques that have not to this point been combined. Both aspects will allow us to produce tools that can be used with realistic code.