Search

The design of complex systems involves several design models supporting different analysis techniques for validation and verification purposes. These activities lead to the definition of heterogeneous modelling languages and analysis techniques. In this setting, meeting certification standards becomes a key issue in system engineering. Reducing heterogeneity due to the presence of different modelling languages can be addressed by providing an integrated framework in which modelling languages and techniques are formalised. In such a framework, checking the global correctness of heterogeneous models of a complex critical system becomes possible in many cases. The work presented in this paper addresses the problem of integrated verification of system design models in the context of transportation systems, in particular railway systems. It has been achieved in context of the B-PERFect project of RATP (Parisian Public Transport Operator and Maintainer) aiming at applying formal verification using the PERF approach on the integrated safety-critical models of embedded software related to railway domain expressed in a single unifying modelling language: HLL. This paper addresses the particular case of the B method. It presents a certified translation of B formal models to HLL models. The proposed approach uses Isabelle/HOL as a unified logical framework to describe the formal semantics and to formalise the transformation relation between both modelling languages. The developed Isabelle/HOL models are proved in order to guarantee the correctness of our translation process. Moreover, we have also used weak-bisimulation relation to check the correctness of each translation step. We also show that, when models are translated into this unified modelling language, it becomes possible to handle the verification of properties expressed across different models. The overall approach is illustrated through a case study issued from a railway software system: on-board localisation function. Furthermore, it discusses the integrated verification at system level.

In order to analyse extensively the safety of the deployed railway software systems, RATP rely on rigorous verification methodologies based on formal methods. During the past few years, RATP has developed a new formal verification method called PERF, supported by a rich proof tool-chain. The main purpose of this method is to perform a non-intrusive verification on the implemented software. Unlike many formal methodologies, it does not require any intervention in the early stages of the software development.

International audience; Formal specifications provide strong bases for testing and bring powerful techniques and technologies. Expressive formal specification languages combine large data domain and behavior. Thus, symbolic methods have raised particular interest for test generation techniques. Integrating formal testing in proof environments such as Isabelle/HOL is referred to as "theorem-prover based testing". Theorem-prover based testing can be adapted to a specific specification language via a representation of its formal semantics, paving the way for specific support of its constructs. The main challenge of this approach is to reduce the gap between pen-and-paper semantics and formal mechanized theories. In this paper we consider testing based on the Circus specification language. This language integrates the notions of states and of complex data in a Z-like fashion with communicating processes inspired from CSP. We present a machine-checked formalization in Isabelle/HOL of this lan- guage and its testing theory. Based on this formal representation of the semantics we revisit the original associated testing theory. We discovered unforeseen simplifications in both definitions and symbolic computations. The approach lends itself to the construction of a tool, that directly uses semantic definitions of the language as well as derived rules of its testing theory, and thus provides some powerful sym- bolic computation machinery to seamlessly implement them both in a technical environment.

Certifications of critical security or safety system properties are becoming increasingly important for a wide range of products. Certifying large systems like operating systems up to Common Criteria EAL 4 is common practice today, and higher certification levels are at the brink of becoming reality.

The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's unifying theories of programming (UTP). We develop a machine-checked, formal semantics based on a "shallow embedding" of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and implement tactic support that finally allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus.

In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus. The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.