An example of use of formal methods to debug an embedded software

André Arnold, Didier Bégay, Jean-Pierre Radoux

17 décembre 1996

Résumé

This article releases an industrial experiment of using formal methods to analyze and to debug a system that was shown erroneous by testing. After presenting the industrial context of the experiment, it details the modelling process and the interpretation of the results, in conjunction with the designers of the system.

1 Introduction

1.1 The EUROTRI project

The EUROTRI project was aimed by Schlumberger-Industries to define, conceive, design and develop a static electricity meter with large abilities of tariff programming and distant measuring. As short time of development and low cost of production (ie: use of components at frontier of their technical limits) were the challenges, it has been decided at the very beginning of the project to use formal methods in most steps of it, from feasability study to reception testing. For different reasons, including readability of transition systems by electronic engineers and availability of a powerful model-checker, the Arnold-Nivat model and the MEC tool have been selected, in conjunction with rate monotonic analysis. Another part of the project, the study of the physical layer of the two processors, at the interface of hardware and software, has been released in [3]. The all work has been presented as a thesis by Jean-Pierre Radoux [phd].

2 The OUCABO system

Dealing with an electricity meter, it is a basic feature to iteratively measure N numerical values (such as voltage, intensity and phase) and to process them in the flow. At a given time t, one among the N analog signals is input in the measuring software, by the mean of a 1-in-n multiplexer, driven by an external (external to the software) counter. So we have two counters referring to the same value: an external (hardware) counter, selecting the input signal, an internal (software) counter, processing the input signal, both of them being controled by the same clock.

The first problem we have to deal with is that parasites can impact the links between the common clock and both devices, and thus desynchronize both counters, making the software process erroneously input values.

This can be handled either by identifying each sample transmitted to the software or by periodically synchronizing both counters. The first solution was not relevant for technical reasons, and it has been designed that an output port would be used by the software counter to reset the hardware counter.

In such an embedded system as the electricity meter, various processes have to be activated to ensure the fiability of the apparatus. One of them is the OUCABO system. This system requires a device to be periodically activated and tested. The second problem is that the solution to first problem left no output port available to activate this secondary device, nor input port to test it. The situation on the output port has been handled using the leftmost carry bit of the hardware counter to activate the device : if the software counter does not reset the hardware counter in due time, there occurs an arithmetic overflow and the device is activated.

This solution had been conceived and implemented ignoring formal methods, as an electronic hack to answer a very simple, low-level problem.

2.1 Debugging the OUCABO system

This part of the system had been developped and implemented, and tested using laboratory testing devices to simultaneously measure same signals. Unfortunately, it happened that a very seldom measure difference occurred between testing and tested devices; at first glance, the origin could be hardware, software or a testing protocol error.

Testing such rare behaviours may last a long time, and in order to spare time, a model-checking approach was accepted. Then the system has been modelled using synchronized labeled transition systems. The error and the error rate could be confirmed on a study of synchronized transitions, thus identifying the source of the erroneous behaviour. The bug was fixed in the model and after verification, the system could be efficiently and safely corrected.

2.2 Content of the paper

Instead of reporting the experience as it was, we choose in this paper to construct step by step, in a pedagogical order, the system to model.

3 Synchronized products of transition systems

We model any behaviour using labeled transition systems (LTS), ie: uniquely named states linked by transitions, each of them wearing a non-null string of characters called its label, and due to model what triggers the transition from source state to target state. As same phenomenon can trigger different transitions depending of current state, different transitions can wear same label.

A parameterized LTS is a LTS where boolean properties are defined on states and transitions, and operators allow computation of such properties as deadlocks of loops, etc… using an adapted version of Tarjan’s algorithm and a μ-calculus engine ([phd, :phd]).

Interactions between behaviours is expressed in our synchronous model using correlation of labels: behaviours triggers freely, provided they respect a set of synchronization constraints, expressed as a set of vectors of firing configurations of labels. So we construct the synchronized product of original LTS’s as a LTS where states are vectors of original states, and transitions are labeled by vectors of original labels, restricted to the synchronization constraints. This synchronized transition system models the global behaviour under study. We can apply on it the usual computing of boolean properties.

Both construct of the synchronized product and computing of boolean properties are implemented in the MEC tool.

A complete description of our model and of the power of expression of the properties will be found in [1], and a shorter one illustrated by some demonstrative examples using MEC is given in [2].

4 Hard and soft counters

The system contains a hardware counter modulo N activated by ticks of a clock and able to be reset to 0 by an input signal. If N ticks occur without any reset, a carry bit is set. Each tick of the clock generates an interruption: the interruption routine increments a counter, called channel and initialized to 0, when its value is strictly less than N − 1, and resets it to 0 and sends a reset signal to the hardware counter when it has value N − 1. The code of this interruption routine is thus if channel < N − 1 then increment(channel) else send(reset); channel:=0; endif

4.1 Modeling the hardware counter

The first thing to do is to give a definite value to N. We assume that N has a lesser value than the actual value, say 4, and it will not be difficult to convince oneself that is a quite admissible simplification with respect to the verifications to be done. The hardware counter can have its carry bit set or not. In order to make things easier, we model activity of the carry bit during 3 × N ticks.

Therefore, the hardware counter can be modeled by a transition with thirteen states. A state of the counter is encoded by a two-digit number: the second digit (0,1,2, or 3) represents the value of the counter and the first digit counts the number of carries since its last reset. Two actions can change the state of the counter:

• a tick of the clock, denoted by t,

• a reset signal, denoted by reset.

We also use the null action denoted by e to express that something else may occurs that has no effect on the counter.

In MEC, such a transition system is written

transition_system counter;
00 |-e-> 00, reset-> 00, t-> 01;
01 |-e-> 01, reset-> 00, t-> 02;
02 |-e-> 02, reset-> 00, t-> 03;
03 |-e-> 03, reset-> 00, t-> 10;
10 |-e-> 10, reset-> 00, t-> 11;
11 |-e-> 11, reset-> 00, t-> 12;
12 |-e-> 12, reset-> 00, t-> 13;
13 |-e-> 13, reset-> 00, t-> 20;
20 |-e-> 20, reset-> 00, t-> 21;
21 |-e-> 21, reset-> 00, t-> 22;
22 |-e-> 22, reset-> 00, t-> 23;
23 |-e-> 23, reset-> 00, t-> 30;
<initial={00}>.

4.2 Modeling the software counter

The software counter (i.e., the code above), is similar to the hardware counter: its states are the values of channel and when a tick occurs (action denoted by t) this value changes. However, when this value is 3, a reset signal is immediately sent to the hardware counter before the value becomes 0 (action denoted by reset). Therefore, we get:

transition_system channel_v1;
0 |-e-> 0, t->1;
1 |-e-> 1, t->2;
2 |-e-> 2, t->3;
3 |-e-> 3, t->30;
30|-reset->0;
<initial={0}>.

Remark that when the channel receives a tick in state 3, it goes into an intermediate state 30. In this state it is not allowed to wait (there is no “e-loop”), it has to immediately execute reset and to go into state 0.

4.3 Synchronization constraint

We consider the system composed of the counter and the channel. When a tick occurs, both components react simultaneously by executing a transition labeled by the action t. When the interruption routine sends a reset signal by reset, the counter simultaneously receives this signal and executes reset too. Finally both components can stay idle together. The system together with this synchronization constraint is described by:

synchronization_system s1 <width = 2; list = (counter, channel_v1)>;
(t    .t    );
(reset.reset);
(e    .e    ).

The synchronized product of this system is:

transition_system r1 <width = 2> ;
e(00.0) |- (e.e) -> e(00.0) , (t.t) -> e(01.1) ;
e(01.1) |- (e.e) -> e(01.1) , (t.t) -> e(02.2) ;
e(02.2) |- (e.e) -> e(02.2) , (t.t) -> e(03.3) ;
e(03.3) |- (e.e) -> e(03.3) , (t.t) -> e(10.30);
e(10.30)|- (reset.reset) -> e(00.0);
 < initial = { e(00.0) } >.

and one can see that, excepted when the channel is in its intermediate state 30, the values of the counter and of the channel are the same.

5 Introduction of a mode

Actually, for some reasons relating to the activity of the secondary device via the carry bit, the above system can be in two modes, special and non special. The mode becomes special when an external and uncontrollable event, called start, is generated by the environment of the system; we assume, to simpplify the model, that once in the special mode, the system cannot come back to the normal mode. The only difference between the two modes is that no reset signal is emitted when in special mode, and thus the carry bit will be set to activate the secondary device: if channel < N − 1 then increment(channel) else if mode is not special then send(reset); endif channel:=0; endif

We model the mode by the transition system

transition_system mode_v1;
not_special |-e-> not_special,
              start-> special,
              is_not_special-> not_special;
special |-e-> special,
          is_special-> special;
<initial={not_special}>.

The action start switches the mode from non special to special. The actions is not special and is special allows to know what the mode of the system is.

We now have a system with three components: counter, channel v1, mode v1.

QUESTION 1. Donner les vecteurs de synchronisation décrivant les interactions de ces trois composants. Quels sont les nombres d’états et de transitions du produit synchronisé obtenu?

QUESTION 2. Montrer que start est bien une action incontrôlable.

Let us describe the interactions between these components.

When a tick occurs it is received by counter and channel and has no effect on mode; this is expressed by the synchronisation vector (t.t.e). When the mode becomes special, nothing happens to the counter and the channel: (e.e.start). When the channel is in state 30 it emits a reset signal if and only if the mode is not special. Instead of modeling this situation, we model an equivalent situation: this signal is emitted in any case but it is received by the counter only if the mode is not special, that is expressed by the two vectors

(reset.reset.is not special) and (e.reset.is special). Thus we get the system

synchronization_system s2 <width = 3 ; list = (counter, channel_v1, mode_v1)>;
(t    .t    .e          );
(e    .e    .start      );
(reset.reset.is_not_special);
(e    .reset.is_special );
(e    .e    .e          ).

whose product is

transition_system r2  <width = 3> ;
e(00.0.not_special) |- (e.e.e) -> e(00.0.not_special) ,
        (e.e.start) -> e(00.0.special) ,
        (t.t.e) -> e(01.1.not_special) ;
e(00.0.special) |- (e.e.e) -> e(00.0.special) ,
        (t.t.e) -> e(01.1.special) ;
e(01.1.not_special) |- (e.e.e) -> e(01.1.not_special) ,
        (e.e.start) -> e(01.1.special) ,
        (t.t.e) -> e(02.2.not_special) ;
e(01.1.special) |- (e.e.e) -> e(01.1.special) ,
        (t.t.e) -> e(02.2.special) ;
e(02.2.not_special) |- (e.e.e) -> e(02.2.not_special) ,
        (e.e.start) -> e(02.2.special) ,
        (t.t.e) -> e(03.3.not_special) ;
e(02.2.special) |- (e.e.e) -> e(02.2.special) ,
        (t.t.e) -> e(03.3.special) ;
e(03.3.not_special) |- (e.e.e) -> e(03.3.not_special) ,
        (t.t.e) -> e(10.30.not_special) ;
e(03.3.special) |- (e.e.e) -> e(03.3.special) ,
        (t.t.e) -> e(10.30.special) ;
e(10.30.not_special) |- (reset.reset.is_not_special) -> e(00.0.not_special) ;
e(10.30.special) |- (e.reset.is_special) -> e(10.0.special) ;
e(10.0.special) |- (e.e.e) -> e(10.0.special) ,
        (t.t.e) -> e(11.1.special) ;
e(11.1.special) |- (e.e.e) -> e(11.1.special) ,
        (t.t.e) -> e(12.2.special) ;
e(12.2.special) |- (e.e.e) -> e(12.2.special) ,
        (t.t.e) -> e(13.3.special) ;
e(13.3.special) |- (e.e.e) -> e(13.3.special) ,
        (t.t.e) -> e(20.30.special) ;
e(20.30.special) |- (e.reset.is_special) -> e(20.0.special) ;
e(20.0.special) |- (e.e.e) -> e(20.0.special) ,
        (t.t.e) -> e(21.1.special) ;
e(21.1.special) |- (e.e.e) -> e(21.1.special) ,
        (t.t.e) -> e(22.2.special) ;
e(22.2.special) |- (e.e.e) -> e(22.2.special) ,
        (t.t.e) -> e(23.3.special) ;
e(23.3.special) |- (e.e.e) -> e(23.3.special) ,
        (t.t.e) -> e(30.30.special) ;
e(30.30.special) |- ;
<initial = { e(00.0.not_special) }>.

6 Activation of a secondary device

When the mode is special, the channel 1 of the multiplexer is used to read a value produced by the device that has been activated by the carry bit of the counter. We use an action “read” to explicit the fact that a value is read on this channel coming from the device.

The interruption routine becomes case 0 < channel < N − 1 ⇒ increment(channel); channel = 0 ⇒ channel:=1; if mode is special then read endif; channel = N − 1 ⇒ if mode is not special then send(reset) endif; channel:=0; end that is modeled by slightly modifying the previous model: adding a new intermediate state 01 between 0 and 1.

transition_system channel_v2;
0 |-e-> 0, t->01;
01|-read-> 1;
1 |-e-> 1, t->2;
2 |-e-> 2, t->3;
3 |-e-> 3, t->30;
30|-reset->0;
<initial={0}>.

Indeed when is special mode the secondary device is activated twice and read twice. We introduce a transition system that counts how many times the device has been read.

transition_system device;
0 |-e-> 0, read-> 1;
1 |-e-> 1, read-> 2;
2 |-e-> 2;
<initial = {0}>.

As for the reset signal, the “read” action will be taken into account depending on the mode is special or not.

QUESTION 3. Donner les vecteurs de synchronisation décrivant les interactions de ces quatre composants. Quels sont les nombres d’états et de transitions du produit synchronisé obtenu?

7 Fixing a bug

To behave correctly the system must meet the following property P:

Just after any reading of the device, the number of activations of the device (i.e., the first digit of the state of the hardware counter) must be equal to the number of readings (i.e., the state of device).

The designers of the code were almost sure that this property was true. Experiments showed that indeed it was not, and we introduced the modeling above just to understand how and why it happened.

7.1 Finding the cause of the errors

First, we look at the states reached after any reading of the device.

QUESTION 4. Expliquer comment calculer cet ensemble d’états. Quels sont ceux qui satisfont la contrainte ci-dessus et ceux qui ne la satisfont pas.

by computing

s := tgt(!label[1]="read");
This set contains four states: e(1.01.1.special), e(1.11.1.special), e(2.11.1.special), and e(2.21.1.special).

The second and the fourth ones satisfy the above requirement, while the first and the third do not. This is indeed the bug in the system and is consistent with the experimental observations.

Looking at a path leading to one of those states, one finds

e(0.00.0.is_not_special)|-(e.e.e.start) ->e(0.00.0.special)
                     |-(e.t.t.e)->e(0.01.01.special)
                     |-(read.e.read.is_special)->e(1.01.1.special)

Then one guesses that the problem is probably caused by the mode switching from non special to special while the channel has value 0.

QUESTION 5. Comment peut-on s’assurer que cette hypothèse est correcte?

To check this guess we define the set of transitions where the mode changes and the channel is 0,

cause := !label[4]="start"/\rsrc(!state[3]="0");

and we compute the set of states that can be reached without using these transitions (indeed, there is only one)

reachable:=reach(initial,*-cause);

The intersection of the sets s and reachable contains only two states, e(1.11.1.special) and e(2.21.1.special), and the two incorrect states become unreachable.

7.2 Some predictions

We know that the observed errors are due to the fact that the system switches to special mode when the channel has value 0. Since the start event is randomly distributed, the probability it occurs when channel has value 0 is 1/4 and the misbehaviour of the system should be observed with a frequency of 1/4. The frequency 1/N was experimentally observed, with respect to the actual value N of the software counter. What is more, the fact that the incorrect result of the actual system is caused by one additionnal reading of the inactivated device (when start event arrives on channel 0) was also experimentally confirmed.

7.3 The correction

A solution for avoiding the problem is to force the system to switch to special mode when the channel has not value 0. But there is no possible control on the start event. On the other hand, it is possible to control the time when the mode switches to special. Thus, we “desynchronize” the two actions: when the start signal is received, the mode goes into a special state informing the system that this event has happened, and the system goes from this state to the special mode under control of the interruption routine by the action named switch. Remark that this action can be executed only when the mode is in state request.

transition_system mode_v2;
not_special |-e-> not_special,
          start-> request,
          is_not_special-> not_special;
request |-e-> request,

          switch-> special
          is_request-> request;
special |-e-> special,
          is_special-> special;
<initial={not_special}>.

When setting the channel from 0 to 1 the interruption routine makes the device to be read if the mode is special and do nothing if the mode is not special. If the mode is in the intermediate state request it switches the mode to special. That new value of the mode will have effect at the next read, as if the start event has occurred when the channel has value 1, 2, or 3! Of course, this cause a delay of four additionnal ticks before switching to the special mode, but engineers found it quite acceptable.

QUESTION 6. Ecrire le système de transitions modélisant cette nouvelle routine d’interruption. Donner les vecteurs de synchronisation décrivant les interactions de ce nouveau système. Vérifier que la propriété P (page 6) est maintenant satisfaite.

QUESTION 7. Ecrire le code de cette nouvelle routine.

The new system becomes

synchronization_system s4 <width = 4 ; list =
(device, counter, channel_v2, mode_v2)>;
(e   .t    .t    .e             );
(e   .e    .e    .start         );
(e   .reset.reset.is_not_special);
(e   .e    .reset.is_special    );
(e   .reset.reset.is_request    );
(e   .e    .read .is_not_special);
(read.e    .read .is_special    );
(e.  .e    .read .switch        ).

The corresponding system has 28 states and 31 transitions. Now, the set

s := tgt(!label[1]="read");

contains only the two correct states e(1.11.1.special) and e(2.21.1.special).

Finally it is easy to rewrite the interruption routine so that it conforms to the model above: case 0 < channel < N − 1 ⇒ increment(channel) channel = 0 ⇒ channel := 1;

if mode = special then read;

elsif mode = request then mode := special; endif;

channel = N − 1 ⇒ if mode is not special then send(reset) endif; channel := 0; end

8 Conclusion

We presented a use of formal methods in an unusual context: at testing time, to find out the cause of an error in a system, with respect to the difficulty to show up some seldom behaviours on the bench. The fault of the system was confirmed, and a precise diagnostic set.

Notice however we did not intend to model and verify an implementation: we specified a posteriori the system by abstracting relevant elements with respect to the misbehaviour.

The efficiency of the use of synchronized labeled transition systems for modeling and checking electronic components has been widened to debugging the system in a way efficient for the developpers.

Bibliographie

[1] A. Arnold. Finite transition systems. Semantics of communicating sytems. Prentice-Hall, 1994.

[2] A. Arnold, D. Bégay, P. Crubillé. Construction and analysis of transition systems with MEC. World Scientific Pub., 1994.

[3] D. Bégay, J. Dormoy, P. Félix. An experiment in developing real-time systems using Mec. In Teodor Rus and Charles Rattray, editors, Theories and experiences for real-time system development, volume 2 of AMAST series in Computing, chapter 14, pages 363–388. World Scientific Pub., 1994.

[4] P. Crubillé. Réalisation de l’outil Mec : spécification fonctionnelle et architecture. PhD thesis, Université de Bordeaux I, novembre 1989.

[5] A. Dicky. Une approche algébrique et algorithmique de l’analyse des systèmes de transition. PhD thesis, Université de Bordeaux I, février 1985.

[6] J.-P. Radoux. Utilisation de systèmes de transitions finis pour la conception et le développement d’un système embarqué. PhD thesis, Université de Bordeaux I, mars 1995.