Switch

​
Introduction
This example demonstrates how to specify a stateless function and how to implement it.
Natural Language Description
A railroad switch is a mechanical installation enabling railway trains to be guided from one track to another at a railway junction. The position of the switch is safety-related. We are considering a control/command system in charge of safely determining the position of the switch. Redudancy is mandatory to take into account sensor failures, leading to a switch equipped with 3 sensors to determine its position. These sensors provide 3 measures: m1, m2, and m3.
The possible values are :
normal (right position)
reverse (left position)
void (middle position while the switch is moving from a position to another)
We have to specify a function
1
pos <-- estimate (m1, m2, m3) = ...
Copied!
calculating an estimate of the switch position, considering that:
if at least, one normal and one reverse are measured, then the result is void.
if all measures are void, then the result is void.
in all other cases, it should return normal or reverse
Formal specification
As usual, the modelling solution is not unique.
We could for example make explicit the value of the return value pos for each value of m1, m2, m3. We could also have a more elegant solution, where we are not obliged to list every single case:
1
MACHINE switch
2
SETS
3
    POSITION = {normal,reverse,void}
4
OPERATIONS
5
pos <-- estimate(m1,m2,m3) =
6
    PRE
7
        m1: POSITION &
8
        m2: POSITION &
9
        m3: POSITION
10
    THEN
11
        SELECT
12
            normal: {m1,m2,m3} &
13
            reverse /: {m1,m2,m3}
14
        THEN
15
            pos:=normal
16
        WHEN
17
            reverse: {m1,m2,m3} &
18
            normal /: {m1,m2,m3}
19
        THEN
20
            pos:=reverse
21
        ELSE
22
            pos:=void
23
        END
24
    END
25
END
Copied!
This model doesn’t generate any non-obvious proof obligation, as there is no variable, no invariant and no properties to verify.
The next step of this example is to implement this specification. We are now obliged to make explicit the algorithm:
1
IMPLEMENTATION switch_1
2
REFINES switch
3
OPERATIONS
4
  pos <-- estimate(m1,m2,m3) =
5
    CASE m1 OF
6
            EITHER normal THEN
7
                  IF m2 = reverse or m3 = reverse THEN
8
                        pos:=void
9
                  ELSE
10
                        pos:=normal
11
                  END
12
            OR reverse THEN
13
                  IF m2 = normal or m3 = normal THEN
14
                        pos:=void
15
                  ELSE
16
                        pos:=reverse
17
                  END
18
            ELSE
19
        CASE m2 OF
20
                    EITHER normal THEN
21
                          IF m3 = reverse THEN
22
                                pos:=void
23
                          ELSE
24
                                pos:=normal
25
                          END
26
                    OR reverse THEN
27
                          IF m3 = normal THEN
28
                                pos:=void
29
                          ELSE
30
                                pos:=reverse
31
                          END
32
                    ELSE
33
                          pos:=m3
34
                    END
35
              END
36
        END
37
  END
38
END
Copied!
The implementation is automatically demonstrated to comply with its specification.
Source code generated
The resulting C code, generated by ComenC from the implementation is given below:
switch.h
1
#ifndef _switch_h
2
#define _switch_h
3
​
4
#include <stdbool.h>
5
​
6
typedef enum {
7
   switch__normal,
8
   switch__reverse,
9
   switch__void
10
} switch__POSITION; 
11
​
12
extern void switch__INITIALISATION(void); 
13
​
14
extern void switch__estimate(
15
   switch__POSITION switch__m1,
16
   switch__POSITION switch__m2,
17
   switch__POSITION switch__m3,
18
   switch__POSITION *switch__pos);
19
#endif
Copied!
switch.c
1
#include <stdbool.h>
2
#include "switch.h"
3
​
4
void switch__INITIALISATION(void) {
5
}
6
​
7
void switch__estimate(
8
    switch__POSITION switch__m1,
9
    switch__POSITION switch__m2,
10
    switch__POSITION switch__m3,
11
    switch__POSITION *switch__pos) {
12
​
13
    switch (switch__m1) {
14
        case switch__normal:
15
            if ((switch__m2 == switch__reverse) || (switch__m3 == switch__reverse)) {
16
               *switch__pos = switch__void;
17
            } else {
18
               *switch__pos = switch__normal;
19
            }
20
            break;
21
        case switch__reverse:
22
            if ((switch__m2 == switch__normal) || (switch__m3 == switch__normal)) {
23
               *switch__pos = switch__void;
24
            } else {
25
               *switch__pos = switch__reverse;
26
            }
27
            break;
28
        default:
29
            switch (switch__m2) {
30
                case switch__normal:
31
                    if (switch__m3 == switch__reverse) {
32
                       *switch__pos = switch__void;
33
                    } else {
34
                       *switch__pos = switch__normal;
35
                    }
36
                    break;
37
              case switch__reverse:
38
                   if (switch__m3 == switch__normal) {
39
                      *switch__pos = switch__void;
40
                   } else {
41
                      *switch__pos = switch__reverse;
42
                   }
43
                   break;
44
              default:
45
                  *switch__pos = switch__m3;
46
                  break;
47
      }
48
      break;
49
   }
50
}
Copied!
B Examples - Previous
Fuel Level
Next - B Examples
Security Policy
Last modified 3mo ago
Copy link
Contents
Introduction
Natural Language Description
Formal specification
Source code generated