🧑‍🎓
Training Resources for Atelier B
  • Introduction
  • Guides and Tutorials
    • Installation
    • Training Videos
    • Training Slides
    • Applying the B Method
      • Project Creation
      • Code Generation
      • Mathematical Proof
        • 🔥Writing Mathematical Rules
          • Introduction
          • Introduction to the Theory Language
          • How to write mathematical rules
          • Using Automatic Prover Mechanisms
          • Guards in a nutshell
          • Normalisation of Expressions
          • Common pitfall
          • All guards in the theory language
    • Extending Atelier B
      • Syntax
      • Examples
    • Programming the CLEARSY Safety Platform
  • Examples and Case-studies
    • Fuel Level
    • Switch
    • Security Policy
    • Verified Software Competitions
  • Additional Resources
    • Glossary
    • References
    • Frequently Asked Questions
Powered by GitBook
On this page
  • Introduction
  • Natural Language Description
  • Formal specification
  • Source code generated

Was this helpful?

  1. Examples and Case-studies

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

pos <-- estimate (m1, m2, m3) = ...

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:

MACHINE switch
SETS
    POSITION = {normal,reverse,void}
OPERATIONS
pos <-- estimate(m1,m2,m3) =
    PRE
        m1: POSITION &
        m2: POSITION &
        m3: POSITION
    THEN
        SELECT
            normal: {m1,m2,m3} &
            reverse /: {m1,m2,m3}
        THEN
            pos:=normal
        WHEN
            reverse: {m1,m2,m3} &
            normal /: {m1,m2,m3}
        THEN
            pos:=reverse
        ELSE
            pos:=void
        END
    END
END

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:

IMPLEMENTATION switch_1
REFINES switch
OPERATIONS
  pos <-- estimate(m1,m2,m3) =
    CASE m1 OF
            EITHER normal THEN
                  IF m2 = reverse or m3 = reverse THEN
                        pos:=void
                  ELSE
                        pos:=normal
                  END
            OR reverse THEN
                  IF m2 = normal or m3 = normal THEN
                        pos:=void
                  ELSE
                        pos:=reverse
                  END
            ELSE
        CASE m2 OF
                    EITHER normal THEN
                          IF m3 = reverse THEN
                                pos:=void
                          ELSE
                                pos:=normal
                          END
                    OR reverse THEN
                          IF m3 = normal THEN
                                pos:=void
                          ELSE
                                pos:=reverse
                          END
                    ELSE
                          pos:=m3
                    END
              END
        END
  END
END

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

#ifndef _switch_h
#define _switch_h

#include <stdbool.h>

typedef enum {
   switch__normal,
   switch__reverse,
   switch__void
} switch__POSITION; 

extern void switch__INITIALISATION(void); 

extern void switch__estimate(
   switch__POSITION switch__m1,
   switch__POSITION switch__m2,
   switch__POSITION switch__m3,
   switch__POSITION *switch__pos);
#endif

switch.c

#include <stdbool.h>
#include "switch.h"

void switch__INITIALISATION(void) {
}

void switch__estimate(
    switch__POSITION switch__m1,
    switch__POSITION switch__m2,
    switch__POSITION switch__m3,
    switch__POSITION *switch__pos) {

    switch (switch__m1) {
        case switch__normal:
            if ((switch__m2 == switch__reverse) || (switch__m3 == switch__reverse)) {
               *switch__pos = switch__void;
            } else {
               *switch__pos = switch__normal;
            }
            break;
        case switch__reverse:
            if ((switch__m2 == switch__normal) || (switch__m3 == switch__normal)) {
               *switch__pos = switch__void;
            } else {
               *switch__pos = switch__reverse;
            }
            break;
        default:
            switch (switch__m2) {
                case switch__normal:
                    if (switch__m3 == switch__reverse) {
                       *switch__pos = switch__void;
                    } else {
                       *switch__pos = switch__normal;
                    }
                    break;
              case switch__reverse:
                   if (switch__m3 == switch__normal) {
                      *switch__pos = switch__void;
                   } else {
                      *switch__pos = switch__reverse;
                   }
                   break;
              default:
                  *switch__pos = switch__m3;
                  break;
      }
      break;
   }
}
PreviousFuel LevelNextSecurity Policy

Last updated 3 years ago

Was this helpful?