|
|
Boulanger Jean-Louis Ressource Site |
|
Formalization of Digital Circuits Using the _ Method
Jean-Louis Boulanger , Ammar
Aljer, and
Georges Mariano
Consultant LIFL INRETS[1]
F-59655
Villeneuve d’Ascq, France F-94114 Arcueil Cedex FRANCE
jl.boulanger@wanadoo.fr aljer@lifl.fr Georges.Mariano@inrets.fr
Abstract. The B method is a formal approach covering
all the software development process, through a series of proved refinement
steps. The formal B method is used
in France more and more for the development of safety-critical software for
railway systems. The B method due to J.R Abrial ([1]) is a formal method for
the incremental development of specifications and their refinements down to an
implementation. It is a model-based approach similar to Z and VDM .
The goal of this paper is to show how it is possible to combine the
advantages of the B method in order to design secure[2] digital
circuits that may be easily developed and does not need a design test. The
circuit design may be based on the libraries of well-known circuit design
language like VHDL. Our goal is to make use of B method to produce the
electronic or numeric circuits.
At the beginning, the circuit specifications are written in the abstract machine. The refinement direction is determined by the basic elements which are used to construct the desired circuit. So the designer can orient the development to the needed level. This level can be found as a basic library in B.
We demonstrate how VHDL packages can be tanslated as circuit components
for giving to the designer a high-level view. Using this approach, one can
develop a circuit of which each part of the specification has proved to be
correct. From the B model it is possible to generate the VHDL code. In this
paper, we describes and models some synchronized basic
components which will be then reused. A synchronized circuit is view as a box,
within which an (or more) input line is entering, and out of which an output line (or
more) is emerging. A synchronized circuit is supposed to be synchronized by a
clock. Our aim is to give a general method to model a circuit without knowing
the details of the desired circuit. At first the analogy of development between
the b method and the numeric circuits design is presented. Using this
approach, one can develop a circuit of which each part of the specification is
proved to be correct. A circuit may be easily improved and it may be
integrated with the other elements in the environment to satisfy safety
conditions. The last section of this paper summarises this work and shows its
advantages and disadvantages. This paper continue the
previous work.
We illustrate the method with
an example extract from [2] which describes a fail-safe interface able to
generate the fail-safe signaIs required in this railways system. Actuators
in safety critical systems must be driven by failsafe signais. Under a failure
in the system, such a signal must be either on the correct or on the safe state
(e.g. red colour in traffic contra! lights).
Keywords :
B method, formal development, software verification,
safety-critical applications, VHDL.
Copyright Boulanger Jean-Louis 2000-2002
Dernières modifications
le : 27 janvier 2002