ICTAC 2008
5th International Colloquium on Theoretical Aspects of Computing



INVITED TALKS

Jean-Raymond Abrial:

Title: Using Design Patterns in Formal Methods: an Event-B Approach

Abstract: The design pattern technique has been proposed a long time ago to be used with object oriented technology where it was found to be extremely useful. In this paper, I investigate how the usage of design pattern can be extended to formal methods. I will give examples of using this approach together with Event-B.

-------------------------------------------------------------------------

AUTHOR: Jan Peleska (FME Invited Speaker)
TITLE: A Unified Approach to Abstract Interpretation, Formal Verification and Testing of C/C++ Modules
ABSTRACT:
Starting from the perspective of safety-critical systems development in avionics, railways and the automotive domain, we advocate an integrated verification approach for C/C++ modules combining abstract interpretation, formal verification by model checking and conventional testing. It is illustrated how testing and formal verification can benefit from abstract interpretation results and, vice versa, how test automation techniques may help to reduce the well known problem of false alarms frequently encountered in abstract interpretations. As a consequence, verification tools integrating these different methodologies can provide a wider variety of useful results to their users and facilitate the bug localisation processes involved.  From the practitioners' point of view, our approach is driven by the applicable standards for safety-critical systems development in the railway and avionic domains: The methods and techniques described should help to (1) fulfil the software-quality related requirements of these standards more efficiently and (2) facilitate the formal justification that these requirements have been completely fulfilled.

We present an overview of the methods required to achieve these goals for C/C++ code verification. The tasks involved can be roughly structured into 5 major building blocks: (1) A parser front-end is required to transform the code into an intermediate model representation which is used for the analyses to follow. The intermediate model representation contains a suitably abstracted memory model which helps us to cope with the problems of aliasing, type casts and mixed arithmetic and bit operations typically present in C/C++ code. (2) Verification tasks have to be decomposed into sub-tasks investigating sub-models. A sub-model selector serves for this purpose. (3) Concrete, symbolic and abstract interpreters are required to support the process of constraint generation, the abstract interpreter serving the dual purpose of runtime error checking and of constraint simplification. (4) A constraint generator prepares the logical conditions accumulated by the interpreters for the (5) constraint solver which is needed to calculate concrete solution vectors as well as over and unde approximations of the constraint solution sets.

Our presentation focuses on the interplay between these building blocks and provides references to more detailed elaborations of the technical problems involved.

-------------------------------------------------------------------------

Bill Roscoe:

Title: The three Platonic models of divergence-strict CSP

Abstract: In an earlier paper, the author proved that there were three models of CSP that play a special role amongst the ones based on finite observations: the traces, stable failures and stable revivals models are successively more refined, but all further models refine stable revivals models.  In the present paper we prove the corresponding result for the divergence-strict models: ones that treat any process that can diverge immediately as the least in the refinement order.   We define what it is to be a divergence-strict model, both for general and finitely nondeterministic CSP, and find that in order to get our result we need to add a new but natural operator into the language.