Formal Verification and Automata Abstraction in Esterel

 
 
Esterel de A à Z
6. 
Exec, vérification formelle, HipHop.js
 
Gérard Berry
 
Collège de France
Chaire Algorithmes, machines et langages
Cours du 28 mars 2018
Précédé du séminaire de Lionel Rieg
 
 
Travaille sur les automates explicites (option –A)
Abstraction
 des donn
ées et de
 signaux, r
éduction par
bisimulation observationnelle
 (cf cours du )
Systèmes :
Auto
 
(R. de Simone, D. Vergamini)
 
:
 
calcul efficace des réductions
Autograph
 
(V. Roy)
 
: dessin interactif des automates réduits
   
 (
Auto 
et
 
Autograph
 
ont eu bien d’autres applications)
21/02/2018
 2
G. Berry, Collège de France
V
érification par abstraction d’automates
Tr
è
s utile, mais limit
é par le risque d’explosion des automates
Plus récents : 
UPPAAL
 (c. 30/03/2016), 
CADP
 (c. 06/04/2016)
 
 
21/02/2018
 
 3
 
G. Berry, Collège de France
 
Exemple : robotique en ORRCAD
 
 
21/02/2018
 
 4
 
G. Berry, Collège de France
 
Exemple : robotique en ORRCAD
 
The International Journal
of Robotics Research
,
April 1st, 1998
 
 
Tr
ès utile,
 même si elle 
ne traite pas les donn
ées
Utilisée en grand par 
Dassault Aviation
 et d’autres en
logiciel, puis pour les circuits de contrôle (
Intel
, 
T.I.
, etc.)
Fondée surtout sur le package de BDD 
TiGeR
 (
O. Coudert
,
J-C. Madre
 et 
H. Touati
) et développée par 
A. Bouali
Principe : 
calcul des états atteignables
, après 
abstraction
éventuelles selon les propriétés à prouver
Calcul de 
contre-exemples
 par exploration inverse de
l’espace d’états
21/02/2018
 5
G. Berry, Collège de France
V
érification booléenne par BDDs
Utilit
é majeure aussi dans la 
génération de tests
,
par contre-exemples à des propriétés évidemment fausses
Ascenseur :
Il est impossible de visiter tous les étages et d’y ouvrir la porte
 
21/02/2018
 6
G. Berry, Collège de France
2. Calcul des 
états accessibles (RSS)
(
voir cours du 21 mars 2018)
A chaque étape, 
utiliser 
R
i
 et 
V
 comme
simplifieurs pour 
C
R
R
0 
= 0
R
1 
= 
R
0
C
R
(
R
0
,
V
)
...
R
i+1 
= 
R
i
C
R
(
R
i
,
V
)
R
n+1 
= 
R
n
C
R
(
R
n
,
V
)
=
 R
n 
 RSS=R
n 
 
contre-exemple
 
 
Principe du 
Bounded Model Checking
 (
BMC
)
construire une formule 
SAT
 (contr
ôle) ou 
SMT
 (contrôle +
données) par 
dépliement progressif de l’espace d’états
→ états accessibles en 
1, 2, 3, … transitions
détecte toutes les erreurs, mais on ne sait pas quand…
des méthodes récentes incorporent la recherche automatique
de 
propriétés inductives
 pour la preuve totale
21/02/2018
 7
G. Berry, Collège de France
Bounded Model Checking en SAT / SMT
Pour Esterel v7 : v
érifieur SAT / SMT Prover SL
de 
Prover Technologies
 (
G. Stålmark
)
 
 
21/02/2018
 
 8
 
G. Berry, Collège de France
 
L
’ascenseur en Esterel v7
 
data 
SizeData
 :
    constant 
N
 : integer = 4;
end data
interface 
TimerIntf 
:
   output 
StartTimer
 ;
   input 
TimerExpired
 ;
end interface
 
interface 
ElevatorEngineIntf
 :
   output 
Start
 ;
   output 
Up
;
   output 
Down
 ;
   output 
Stop
 ;
   input 
CabinStopped
 ;
end interface
// This interface comprises the sensors that tell the cabin is reaching a floor.
interface 
FloorSensorIntf
 :
   data 
SizeData
 ;
   input 
ReachingFloor
 [
N
];
end interface
 
 
21/02/2018
 
 9
 
G. Berry, Collège de France
 
interface 
CabinIntf
 :
   
// user door control buttons
   input 
DoorOpen
 ;
   input 
DoorClose
 ;
  
 // the sensor unit that signals traversal of door ( light cell ) and shocks
   input 
DoorSensor
 ;
   
// the sensors that signals proper door opening and closing
   input 
DoorIsOpen
 ;
   input 
DoorIsClosed
 ;
   
// basic input relations
   input relation 
DoorIsClosed 
# 
DoorSensor 
;
   input relation 
DoorIsClosed
 # 
DoorOpen
 ; 
// Alfred de Musset
   
// commands to drive door opening and closing motors
   output 
OpenDoorMotorOn
 ;
   output 
OpenDoorMotorOff
 ;
   output 
CloseDoorMotorOn
 ;
   output 
CloseDoorMotorOff
 ;
end interface
 
 
21/02/2018
 
10
 
G. Berry, Collège de France
 
interface 
ButtonsAndLightsIntf
 :
data 
SizeData
 ;
input 
CabinCall
 [
N
];                 
// numbered buttons in the cabin
input 
UpCall
 [
N
];                      
// up buttons at floors (fake one at floor N -1)
input 
DownCall
 [
N
];                  
// down buttons at floors (fake one at floor 0)
output 
CurrentUp
 ;                   
// up arrows at floors and in cabin
output 
CurrentDown
 ;               
// down arrows at floors and in cabin
output 
CurrentFloor
 [
N
];           
// to light up current floor number (one-hot array )
output 
StoppedAtFloor
 [
N
];      
// triggers a bell at floor
output 
PendingCabinCall
 [
N
];  
// sent to the cabin floor button lights
output 
PendingUpCall
 [
N
];       
// sent to floor up button lights
output 
PendingDownCall
 [
N
];  
// sent to floor down button lights
output 
PendingCall
 [
N
];           
// some pending call at floor N
end interface
 
 
21/02/2018
 
11
 
G. Berry, Collège de France
 
module Cabin :
   extends 
TimerIntf
 ;
   extends 
CabinIntf
 ;
   input 
CabinStopped
 ; 
// the signal that tells the elevator is stopped
  
 loop
      trap 
Done
 in
         loop
            emit 
OpenDoorMotorOn
 ;
            await 
DoorIsOpen
 ;
            emit 
OpenDoorMotorOff
 ;
            abort
               finalize
                  emit 
StartTimer
 ;
                  await 
TimerExpired
 or 
DoorClose
 ;
                  emit 
CloseDoorMotorOn
 ;
                  await 
DoorIsClosed
 ;
                  exit 
Done
               with
                  emit 
CloseDoorMotorOff
 ;
               end finalize
            when 
DoorOpen
 or 
DoorSensor
         end loop
      end trap;
      await 
CabinStopped
   end loop
end module
 
 
21/02/2018
 
12
 
G. Berry, Collège de France
 
module 
CallHandler
 :
   data 
SizeData
 ;
   extends 
ButtonsAndLightsIntf
 ;
   extends 
ElevatorEngineIntf
 ;
   extends 
FloorSensorIntf
 ;
input 
DoorIsClosed
 ; 
// from cabin
signal 
CallToGoUp
 , 
CallToGoDown
 in
   
<compute current floor and decide whether to stop >
||
   <compute StoppedAtFloor [i] for each floor i>
||
   <compute pending calls >
||
   <compute calls to go up or down >
||
   <compute CurrentUp or CurrentDown directions >
||
   <start motor in appropriate direction >
||
   <internal consistency assertions >
end signal
end module
 
 
21/02/2018
 
13
 
G. Berry, Collège de France
 
<compute current floor and decide whether to stop>
 
emit 
CurrentFloor
 [1];
always
   signal ReachingSomeFloor in
      for 
i
 < 
N
 dopar
         if 
ReachingFloor
 [
i
] then
            emit 
ReachingSomeFloor
 ;
           
 // set current floor i; automatically resets previous current floor
            emit 
CurrentFloor
 [
i
];
            // we have to stop if we are moving in a direction and
            // either there is a floor call for the same direction at this floor
            // or there is no more call at further floors in the same direction
            // warning : we have to take pre( CurrentUp ) because CurrentUp
            // is reset in the instant if there is no call up
            if ((pre(
CurrentUp
 ) and (
PendingUpCall
 [
i
] or not 
CallToGoUp
))
                or (pre(
CurrentDown
 ) and ( 
PendingDownCall
 [
i
] or not 
CallToGoDown
)))
            then
               emit 
Stop
            end
         else
            // not reaching floor i , we simply need to cancel potential current
            // floor emission if some other floor has just been reached .
            emit 
CurrentFloor
 [
i
] <= pre( 
CurrentFloor
 [
i
]) and not 
ReachingSomeFloor
         end if
      end for
   end signal
end always
 
 
21/02/2018
 
 14
 
G. Berry, Collège de France
 
<compute StoppedAtFloor [i] for each floor i>
 
weak abort
   sustain 
StoppedAtFloor
 [1]
when 
Start
 ;
for 
i
 < 
N
 dopar
   loop
      await 
ReachingFloor
 [
i
] and 
Stop
 ;
      await 
CabinStopped
 ;
      weak abort
         sustain 
StoppedAtFloor
 [
i
]
      when 
Start
   end loop
end for
 
 
21/02/2018
 
 15
 
G. Berry, Collège de France
 
<compute pending calls >
 
for
 i
 < 
N
 dopar
   always
      if (not 
StoppedAtFloor
 [i]) then
         
emit {
            
PendingCabinCall
 [i] <= 
CabinCall
 [i] or pre(
PendingCabinCall
 [i]),
            
PendingUpCall
 [i] <= 
UpCall
 [i] or pre(
PendingUpCall
 [i]),
            
PendingDownCall
 [i] <= 
DownCall
 [i] or pre( 
PendingDownCall
 [i]),
            
PendingCall
 [i] = 
PendingCabinCall
 [i]
                                       
or 
PendingUpCall
 [i] or 
PendingDownCall
 [i],
         
}
      
end if
   end always
end for
 
 
21/02/2018
 
 16
 
G. Berry, Collège de France
 
 <compute calls to go up or down >
 
   signal 
AuxUpFloor
 [
N
], 
AuxCallToGoUp
 [
N
] in
      sustain {
         seq {
            for 
i 
< 
N
 -1 doup
               AuxUpFloor [
i
+1] <= 
CurrentFloor
 [
i
] or 
AuxUpFloor
 [
i
],
               
AuxCallToGoUp
 [
i
+1] <= (
PendingCall
 [
i
+1] and 
AuxUpFloor
 
[i
+1])
                                                        or 
AuxCallToGoUp
 [
i
]
            end for
         },
         
CallToGoUp
 <= 
AuxCallToGoUp
 [
N
 -1]
      }
   end signal
||
   // computing whether there is a call for going down
   // Warning : this code uses a combinational down carry chain
   signal 
AuxDownFloor
 [
N
], 
AuxCallToGoDown
 [
N
] in
      sustain {
         seq {
            for
 i
 < 
N
 -1 dodown
               
AuxDownFloor
 [
i
] <= 
CurrentFloor
 [
i
+1] or 
AuxDownFloor
 [
i
+1] ,
               
AuxCallToGoDown
 [
i
] <= (
PendingCall
 [
i
] and 
AuxDownFloor
 [
i
])
                                                       or 
AuxCallToGoDown
 [
i
+1]
             end for
         },
         
CallToGoDown
 <= 
AuxCallToGoDown
 [0]
      }
   end signal
 
 
21/02/2018
 
 17
 
G. Berry, Collège de France
 
 <compute CurrentUp or CurrentDown directions >
 
loop
   await
      case immediate 
CallToGoUp
 do
         abort
            sustain 
CurrentUp
         when not 
CallToGoUp
      case immediate 
CallToGoDown
 do
         abort
            sustain 
CurrentDown
         when not 
CallToGoUp
   end await
end loop
 
 
21/02/2018
 
 18
 
G. Berry, Collège de France
 
 <start motor in appropriate direction >
 
loop
   await 
StartOK
 ;
   await immediate 
CallToGoUp
 or 
CallToGoDown
 ;
   emit 
Start
 ;
   if
      case pre(
CurrentUp
) and 
CallToGoUp
 do
         emit 
Up
      case pre(
CurrentDown
 ) and 
CallToGoDown
 do
         emit 
Down
      case 
CallToGoUp
 do
         emit 
Up
      case 
CallToGoDown
 do
         emit 
Down
   end if
end loop
 
 
21/02/2018
 
 19
 
G. Berry, Collège de France
 
Assertions de coh
érence interne
 
sustain {
   
// there is always a direction given at start time
   assert 
SomeDirection
 = 
Start
 => (
Up
 or 
Down
),
   // always start up at bottom floor
   assert 
NoBottomCrash
 = (
StoppedAtFloor
 [0] and 
Start
 ) => 
Up
 ,
   // always start down at top floor
   assert 
NoTopCrash
 = (
StoppedAtFloor
 [N -1] and 
Start
 ) => 
Down
 ,
   // tell stopped at only one floor at a time (as is, not parametric in N)
   assert 
StopOK
 =   
StoppedAtFloor
 [0] # 
StoppedAtFloor
 [1]
                              # 
StoppedAtFloor
 [2] # 
StoppedAtFloor
 [3]
}
 
21/02/2018
 20
G. Berry, Collège de France
V
érification par 
observateurs
 (N. Halbwachs)
Env 
Prog
Obs
E
BUG
Pour toutes les s
équences d’entrée
 
OK
,
l
’observateur n’émet jamais 
BUG
OK
 
 
21/02/2018
 
 21
 
G. Berry, Collège de France
 
Assertion temporelle :
l
’ascenseur ne voyage pas la porte ouverte
 
signal 
Running
 in
   loop
      await 
Start 
;
      abort
           sustain 
Running
      when 
CabinStopped
   
end loop
||
   
loop
      
await 
OpenDoorMotorOn
 
;
      abort
          sustain 
assert
 
DoorOpenedWhenMovingBug 
if 
Running
     
 when 
DoorIsClosed
   end loop
end signal
 
Mais l
’ascenseur n’évolue pas dans un
environnement physique quelconque !
 
caractérisation  de l’environnement,
     indispensable pour 
vérifier les propriétés
 et
     produire des 
contre-exemples pertinents
     en 
réduisant les entrées et l’espace d’états
21/02/2018
 22
G. Berry, Collège de France
D
éfinition de l’environnement
La caract
érisation de l’environnement est
souvent longue et délicate !
… mais elle nous en apprend beaucoup
 
21/02/2018
 23
G. Berry, Collège de France
Contraintes d
’environnement de l’ascenseur
trap 
Bad
 in
   always
      
// no up call button at top floor
      if 
UpCall
 [
N
-1] then exit 
Bad
 end
   ||
      
// no down call button at bottom floor
      if 
DownCall
 [0] then exit 
Bad
 end
   ||
      
// elevator is at most at one floor at a time
      if not (    
ReachingFloor
 [0]
                 # 
ReachingFloor
 [1]
                 # 
ReachingFloor
 [2]
                 # 
ReachingFloor
 [3] ) then
         exit 
Bad
      end if
   ||
      
// A door must be open or closed ( Musset )
      if not ( 
DoorIsOpen
 # 
DoorIsClosed
 ) then
         exit 
Bad
      end if
   end always
 
 
21/02/2018
 
 24
 
G. Berry, Collège de France
 
Contraintes d
’environnement de l’ascenseur
 
   ||
      // at most one TimerExpired after StartTimer
      abort
         every immediate 
TimerExpired 
do exit 
Bad
 end
      when 
StartTimer
 ;
      loop
         if 
TimerExpired
 then exit 
Bad
 end;
         await 
TimerExpired
 ;
         every 
TimerExpired
 do exit 
 
 end
      each 
StartTimer
   ||
      
// at most one CabinStopped with one tick to react
      loop
         weak abort
            every immediate 
CabinStopped
 do exit 
Bad
 end
         when Stop ;
         await 
CabinStopped
 ;
         pause
      end loop
 
 
 
21/02/2018
 
 25
 
G. Berry, Collège de France
 
Contraintes d
’environnement de l’ascenseur
 
   ||
      signal 
ReachingSomeFloor
 , 
ShiftedCurrentFloor
 [N+3] ,
                 
MovingUp
 , 
MovingDown
 in
         sustain {
            for 
i 
< 
N
 dopar
              
ReachingSomeFloor
 <= 
ReachingFloor
 [i]
            end for
         }
      ||
         
// cannot reach a floor between Stop and Start
         loop
            weak abort
               every 
ReachingSomeFloor
 do exit 
Bad
 end
            when 
Start
 ;
            await 
Stop
         
end loop
 
 
 
21/02/2018
 
 26
 
G. Berry, Collège de France
 
Contraintes d
’environnement de l’ascenseur
 
  
 
||
      signal
 
ReachingSomeFloor , ShiftedCurrentFloor [N+3] ,
                 MovingUp , MovingDown
 
in
      
||
         
// when at floor i , the next floor is necessarily i+1 or i-1
         loop
            abort
               sustain {
                  for i < N do
                     
ShiftedCurrentFloor
 [i+1] <= pre( 
ShiftedCurrentFloor
 [i+1])
                  end for
                }
            when immediate 
ReachingSomeFloor
 ;
            emit {
               for i < N do
                  
ShiftedCurrentFloor
 [i +1] <= 
ReachingFloor
 [i]
               end for
            };
            pause
        end loop
 
 
 
21/02/2018
 
 27
 
G. Berry, Collège de France
 
Contraintes d
’environnement de l’ascenseur
 
  
 
||
      signal
 
ReachingSomeFloor , ShiftedCurrentFloor [N+3] ,
                 MovingUp , MovingDown
 
in
      
||
         loop
            await 
Start
 ;
            weak abort
               if
                  case 
Up
 do sustain 
MovingUp
                  case 
Down
 do sustain 
MovingDown
                  default do emit 
Ignore
               end if
            when 
Stop
         end loop
 
21/02/2018
 28
G. Berry, Collège de France
Contraintes d
’environnement de l’ascenseur
 
  
 
||
      signal
      ||
         emit 
ShiftedCurrentFloor
 [2] ;
         weak abort
            every immediate 
ReachingSomeFloor
 do exit 
Bad
 end
         when 
Start
 ;
         loop
            await 
ReachingSomeFloor
 ;
            for 
i
<
N
 dopar
               if 
ReachingFloor
 [
i
] then
                  if 
MovingUp
 and not pre(
ShiftedCurrentFloor
 [
i
]) then
                     exit 
Bad
                  end if ;
                  if 
MovingDown
 and not pre(
ShiftedCurrentFloor
 [
i
+2]) then
                     exit 
Bad
                  end if ;
               end if
            end for
         end loop
      end signal
   handle 
Bad
 do
      emit 
Ignore
   end trap
end module
 
 
 
1. La v
érification formelle en Esterel
2. Interfacer le code g
énéré et le simuler
 
21/02/2018
 
 29
 
G. Berry, Collège de France
 
Agenda
 
 
En circuits
 : engendrer du Verilog, utiliser une CAO
standard
En logiciel :
 plusieurs mani
ères équivalentes d’engendrer
un code C (ou C++, etc.), et plusieurs façons de l’intégrer
dans du code plus général
principe : 
définir des fonctions associées aux sorties,
donner les entrées, appeler la fonction de réaction
pas de contrainte spécifique sur quand et comment
mais une 
contrainte absolue
 : 
l’exécution du code de la
fonction de réaction doit être
 
atomique
.
en particulier,
 
les valeurs des entrées doivent rester
constantes
 
pendant toute la réaction
21/02/2018
 30
G. Berry, Collège de France
Comment ex
écuter un programme
Esterel
 
 
21/02/2018
 
 31
 
G. Berry, Collège de France
 
Exemple pour ABRO
 
void 
ABRO_
O_
O () {
   printf(”O emitted\n”);
}
void main () {
   
ABRO_reset
 
();  
// ABRO initialization
   
ABRO
 
();            
// empty tick
   
ABRO_I_
A
 
(); 
    
// input A
   
ABRO_I_
B
 
();
     
// input B, same instant
   
ABRO
 
();         
  
 
// tick, emits O
   
ABRO_I_
R
 
();  
  
 
// input R, reset
}
 
BLEU :
 
à définir par l’utilisateur
MARRON :
 défini par le compilateur Esterel
 
 
Seule chose 
à définir : les types et fonctions de données
Trois types de simulation :
textuelle : 
entrée des signaux au terminal ou par fichier
textuelle : 
traçage optionnel des signaux, variables, etc.
graphique :
 
xes
, 
Esterel Studio
textuelle :    
entrées par clics, sorties visuelles
                        animation colorée du code source
mixte : 
magnétophone dans les simulateurs graphiques
mixte : 
lisant et écrivant les formats textuels
 
21/02/2018
 
 32
 
G. Berry, Collège de France
 
Simuler un programme Esterel
Usage : 
debugging, non-r
égression,
exécution des tests engendrés automatiquement,
visulalisation des contre-exemples 
de v
érification
 
 
1. La v
érification formelle en Esterel
2. Interfacer le code g
énéré et le simuler
3. Exec : contrôle d’activités asynchrones
 
21/02/2018
 
 33
 
G. Berry, Collège de France
 
Agenda
 
Id
ée : appeler des fonctions (ou tâches) exécutées de
façon asynchrone
Attendre leur retour pour terminer au sens d’Esterel, lors
d’un instant 
suivant
Les suspendre ou les tuer si l’instruction exec est
suspendue ou tuée par Esterel suspend, abort, exit, etc.
21/02/2018
 34
G. Berry, Collège de France
L
’instruction Exec
Usage : 
calculs longs, appels r
éseaux,
mouvements de bras de robots, etc.
 
21/02/2018
 35
G. Berry, Collège de France
Exemple
input 
A
, 
B
, 
X
;
return 
R
;
var 
V
, 
W
 : integer in
   loop
      suspend
         weak abort 
            exec Task (
V
, 
W
)(?
X
+1)
         when 
B
 
      when 
A
   
end loop
end var
 
valeurs et retours
par r
éférence
 
valeurs
r
éincarnation 
 
passer un unique id à chaque appel
 
 
21/02/2018
 
 36
 
G. Berry, Collège de France
 
Interface bas niveau d
’Exec (Esterel v5)
 
typedef struct {
   unsigned int 
start
 : 1
 
;
   unsigned int 
kill
 : 1 ;
   unsigned int 
active
 : 1 ;
   unsigned int 
suspended
 : 1 ;
   unsigned int 
prev_active
 : 1 ;
   unsigned int
 prev_suspended
 : 1 ; 
/* to generate suspend / resume */
   unsigned int
 exec_index 
;              
/* unique id in the program */
   unsigned int 
task_exec_index 
;     
/* unique run-time id*/
   void (*pStart)() ;                             
/* takes a function as argument */
   int (*pRet)() ;                                  
/* may take a value as argument */
} 
__ExecStatus 
;
 
21/02/2018
 37
G. Berry, Collège de France
Interface haut niveau d
’Exec (Esterel v5)
 
#include "exec_status.h"
my_start
 () { ... }
my_kill
 () { ... }
my_suspend
 () { ... }
my_resume
 () { ... }
 
STD_EXEC
 (
R1
, 
REACT
, 
my_start_1
, 
my_kill_1
, 
my_suspend_1
, 
my_resume_1
);
 
STD_EXEC
 (
R2
, 
REACT
, 
my_start_2
, 
my_kill_2
, 
my_suspend_2
, 
my_resume_2
);
 
/*engendrer automatiquement un STD_EXEC pour chaque t
âche */
STD_EXEC_FOR_TASK
 (
TASK
, 
REACT
,
                                         
my_start
, 
my_kill
, 
my_suspend
, 
my_resume
);
Pr
écis, mais assez lourd à l’usage
Très simplifé en HipHop.js (programmation fonctionnelle) 
 
 
21/02/2018
 
38
 
G. Berry, Collège de France
 
function 
execColor
(
langPair
) {
 
   return 
MODULE
 (
IN
 
text
, 
OUT
 
color
, 
OUT
 
trans
, 
OUT
 
error
) {
 
      
EMIT
 
color
("red");
 
      
AWAIT
 
IMMEDIATE
(
NOW
(
text
));
 
      
PROMISE
 
trans
, 
error
 
translate
(langPair, 
VAL
(
text
));
 
      
EMIT
 color("green");
 
   }
 
}
        window.onload = function() {
 
   hh = require("hiphop");
 
   
m = new hh.
ReactiveMachine
(
MODULE
 (
IN
 
text
,
  
                                                   
OUT
 
transEn
, 
OUT
 
colorEn
,
   
                                
OUT
 
transNe
, 
OUT
 
colorNe
,
    
              
OUT
 
transEs
, 
OUT
 
colorEs
,
    
              
OUT
 
transSe
, 
OUT
 
colorSe
) {
 
      
LOOPEACH
(
NOW
(
text
)) {
  
 
FORK
 {
  
    
RUN
(
execColor
("fr|en"), 
color
=
colorEn
, 
trans
=
transEn
);
  
 } PAR {
  
    
RUN
(
execColor
("en|fr"), 
color
=
colorNe
, 
text
=
transEn
, 
trans
=
transNe
);
  
 } PAR {
  
    
RUN
(
execColor
("fr|es"), 
color
=
colorEs
, 
trans
=
transEs
);
  
 } PAR {
  
    
RUN
(
execColor
("es|fr"), 
color
=
colorSe
, 
text
=
transEs
, 
trans
=
transSe
);
  
 }
 
      }
 
   }, {debuggerName: "debug"});
 
}
     }
 
 
Version JavaScript de HiHop, dont la version Scheme a
été présentée avec M. Serrano le
 
21/02/2018
 
 39
 
G. Berry, Collège de France
 
HipHop.js
 
 
21/02/2018
 
 40
 
G. Berry, Collège de France
 
 
exec-statement:
 
EXEC 
exec-start
 
exec-paramsopt
 
EXECEMIT 
identifier
 
exec-start exec-params
opt
 
PROMISE 
identifier
, 
identifier
 
exec-start exec-params
opt
exec-start:
 
js-bridge
 
DONE
 
DONEREACT
exec-params:
 
ONSUSP 
js-bridge
 
ONRES 
js-bridge
 
ONKILL 
js-bridge
js-bridge:
 
instruction
JS
 
THIS
Slide Note
Embed
Share

This content delves into the applications of formal verification and automata abstraction in Esterel, focusing on techniques such as verification by abstraction of automata, boolean verification using BDDs, bounded model checking in SAT/SMT, and more. The work of Gérard Berry at the Collège de France is highlighted, emphasizing practical examples in robotics and software verification. The use of tools like TiGeR, UPPAAL, and CADP is discussed, showcasing how these techniques are applied in real-world scenarios to verify complex systems.


Uploaded on Aug 27, 2024 | 0 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

E N D

Presentation Transcript


  1. Esterel de A Z 6. Exec, v rification formelle, HipHop.js G rard Berry Coll ge de France Chaire Algorithmes, machines et langages Cours du 28 mars 2018 Pr c d du s minaire de Lionel Rieg gerard.berry@college-de-france.fr http://www-sop.inria.fr/members/Gerard.Berry

  2. Vrification par abstraction dautomates Travaille sur les automates explicites (option A) Abstraction des donn es et de signaux, r duction par bisimulation observationnelle (cf cours du ) Syst mes : Auto (R. de Simone, D. Vergamini) : calcul efficace des r ductions Autograph (V. Roy) : dessin interactif des automates r duits (Auto et Autograph ont eu bien d autres applications) Tr s utile, mais limit par le risque d explosion des automates Plus r cents : UPPAAL (c. 30/03/2016), CADP (c. 06/04/2016) G. Berry, Coll ge de France 21/02/2018 2

  3. Exemple : robotique en ORRCAD G. Berry, Coll ge de France 21/02/2018 3

  4. Exemple : robotique en ORRCAD The International Journal of Robotics Research, April 1st, 1998 G. Berry, Coll ge de France 21/02/2018 4

  5. Vrification boolenne par BDDs Tr s utile, m me si elle ne traite pas les donn es Utilis e en grand par Dassault Aviation et d autres en logiciel, puis pour les circuits de contr le (Intel, T.I., etc.) Fond e surtout sur le package de BDD TiGeR (O. Coudert, J-C. Madre et H. Touati) et d velopp e par A. Bouali Principe : calcul des tats atteignables, apr s abstraction ventuelles selon les propri t s prouver Calcul de contre-exemples par exploration inverse de l espace d tats Utilit majeure aussi dans la g n ration de tests, par contre-exemples des propri t s videmment fausses Ascenseur : Il est impossible de visiter tous les tages et d y ouvrir la porte G. Berry, Coll ge de France 21/02/2018 5

  6. 2. Calcul des tats accessibles (RSS) (voir cours du 21 mars 2018) V I O C CR R contre-exemple R0 = 0 R1 = R0 CR(R0,V) ... Ri+1 = Ri CR(Ri,V) Rn+1 = Rn CR(Rn,V)= Rn RSS=Rn A chaque tape, utiliser Riet V comme simplifieurs pour CR G. Berry, Coll ge de France 21/02/2018 6

  7. Bounded Model Checking en SAT / SMT Principe du Bounded Model Checking (BMC) construire une formule SAT (contr le) ou SMT (contr le + donn es) par d pliement progressif de l espace d tats tats accessibles en 1, 2, 3, transitions d tecte toutes les erreurs, mais on ne sait pas quand des m thodes r centes incorporent la recherche automatique de propri t s inductives pour la preuve totale Pour Esterel v7 : v rifieur SAT / SMT Prover SL de Prover Technologies (G. St lmark) G. Berry, Coll ge de France 21/02/2018 7

  8. Lascenseur en Esterel v7 data SizeData : constant N : integer = 4; end data interface TimerIntf : output StartTimer ; input TimerExpired ; end interface interface ElevatorEngineIntf : output Start ; output Up; output Down ; output Stop ; input CabinStopped ; end interface // This interface comprises the sensors that tell the cabin is reaching a floor. interface FloorSensorIntf : data SizeData ; input ReachingFloor [N]; end interface G. Berry, Coll ge de France 21/02/2018 8

  9. interface CabinIntf : // user door control buttons input DoorOpen ; input DoorClose ; // the sensor unit that signals traversal of door ( light cell ) and shocks input DoorSensor ; // the sensors that signals proper door opening and closing input DoorIsOpen ; input DoorIsClosed ; // basic input relations input relation DoorIsClosed # DoorSensor ; input relation DoorIsClosed # DoorOpen ; // Alfred de Musset // commands to drive door opening and closing motors output OpenDoorMotorOn ; output OpenDoorMotorOff ; output CloseDoorMotorOn ; output CloseDoorMotorOff ; end interface G. Berry, Coll ge de France 21/02/2018 9

  10. interface ButtonsAndLightsIntf : data SizeData ; input CabinCall [N]; // numbered buttons in the cabin input UpCall [N]; // up buttons at floors (fake one at floor N -1) input DownCall [N]; // down buttons at floors (fake one at floor 0) output CurrentUp ; // up arrows at floors and in cabin output CurrentDown ; // down arrows at floors and in cabin output CurrentFloor [N]; // to light up current floor number (one-hot array ) output StoppedAtFloor [N]; // triggers a bell at floor output PendingCabinCall [N]; // sent to the cabin floor button lights output PendingUpCall [N]; // sent to floor up button lights output PendingDownCall [N]; // sent to floor down button lights output PendingCall [N]; // some pending call at floor N end interface G. Berry, Coll ge de France 21/02/2018 10

  11. module Cabin : extends TimerIntf ; extends CabinIntf ; input CabinStopped ; // the signal that tells the elevator is stopped loop trap Done in loop emit OpenDoorMotorOn ; await DoorIsOpen ; emit OpenDoorMotorOff ; abort finalize emit StartTimer ; await TimerExpired or DoorClose ; emit CloseDoorMotorOn ; await DoorIsClosed ; exit Done with emit CloseDoorMotorOff ; end finalize when DoorOpen or DoorSensor end loop end trap; await CabinStopped end loop end module G. Berry, Coll ge de France 21/02/2018 11

  12. module CallHandler : data SizeData ; extends ButtonsAndLightsIntf ; extends ElevatorEngineIntf ; extends FloorSensorIntf ; input DoorIsClosed ; // from cabin signal CallToGoUp , CallToGoDown in <compute current floor and decide whether to stop > || <compute StoppedAtFloor [i] for each floor i> || <compute pending calls > || <compute calls to go up or down > || <compute CurrentUp or CurrentDown directions > || <start motor in appropriate direction > || <internal consistency assertions > end signal end module G. Berry, Coll ge de France 21/02/2018 12

  13. <compute current floor and decide whether to stop> emit CurrentFloor [1]; always signal ReachingSomeFloor in for i < N dopar if ReachingFloor [i] then emit ReachingSomeFloor ; // set current floor i; automatically resets previous current floor emit CurrentFloor [i]; // we have to stop if we are moving in a direction and // either there is a floor call for the same direction at this floor // or there is no more call at further floors in the same direction // warning : we have to take pre( CurrentUp ) because CurrentUp // is reset in the instant if there is no call up if ((pre(CurrentUp ) and (PendingUpCall [i] or not CallToGoUp)) or (pre(CurrentDown ) and ( PendingDownCall [i] or not CallToGoDown))) then emit Stop end else // not reaching floor i , we simply need to cancel potential current // floor emission if some other floor has just been reached . emit CurrentFloor [i] <= pre( CurrentFloor [i]) and not ReachingSomeFloor end if end for end signal end always G. Berry, Coll ge de France 21/02/2018 13

  14. <compute StoppedAtFloor [i] for each floor i> weak abort sustain StoppedAtFloor [1] when Start ; for i < N dopar loop await ReachingFloor [i] and Stop ; await CabinStopped ; weak abort sustain StoppedAtFloor [i] when Start end loop end for G. Berry, Coll ge de France 21/02/2018 14

  15. <compute pending calls > for i < N dopar always if (not StoppedAtFloor [i]) then emit { PendingCabinCall [i] <= CabinCall [i] or pre(PendingCabinCall [i]), PendingUpCall [i] <= UpCall [i] or pre(PendingUpCall [i]), PendingDownCall [i] <= DownCall [i] or pre( PendingDownCall [i]), PendingCall [i] = PendingCabinCall [i] or PendingUpCall [i] or PendingDownCall [i], } end if end always end for G. Berry, Coll ge de France 21/02/2018 15

  16. <compute calls to go up or down > signal AuxUpFloor [N], AuxCallToGoUp [N] in sustain { seq { for i < N -1 doup AuxUpFloor [i+1] <= CurrentFloor [i] or AuxUpFloor [i], AuxCallToGoUp [i+1] <= (PendingCall [i+1] and AuxUpFloor [i+1]) or AuxCallToGoUp [i] end for }, CallToGoUp <= AuxCallToGoUp [N -1] } end signal || // computing whether there is a call for going down // Warning : this code uses a combinational down carry chain signal AuxDownFloor [N], AuxCallToGoDown [N] in sustain { seq { for i < N -1 dodown AuxDownFloor [i] <= CurrentFloor [i+1] or AuxDownFloor [i+1] , AuxCallToGoDown [i] <= (PendingCall [i] and AuxDownFloor [i]) or AuxCallToGoDown [i+1] end for }, CallToGoDown <= AuxCallToGoDown [0] } end signal G. Berry, Coll ge de France 21/02/2018 16

  17. <compute CurrentUp or CurrentDown directions > loop await case immediate CallToGoUp do abort sustain CurrentUp when not CallToGoUp case immediate CallToGoDown do abort sustain CurrentDown when not CallToGoUp end await end loop G. Berry, Coll ge de France 21/02/2018 17

  18. <start motor in appropriate direction > loop await StartOK ; await immediate CallToGoUp or CallToGoDown ; emit Start ; if case pre(CurrentUp) and CallToGoUp do emit Up case pre(CurrentDown ) and CallToGoDown do emit Down case CallToGoUp do emit Up case CallToGoDown do emit Down end if end loop G. Berry, Coll ge de France 21/02/2018 18

  19. Assertions de cohrence interne sustain { // there is always a direction given at start time assert SomeDirection = Start => (Up or Down), // always start up at bottom floor assert NoBottomCrash = (StoppedAtFloor [0] and Start ) => Up , // always start down at top floor assert NoTopCrash = (StoppedAtFloor [N -1] and Start ) => Down , // tell stopped at only one floor at a time (as is, not parametric in N) assert StopOK = StoppedAtFloor [0] # StoppedAtFloor [1] # StoppedAtFloor [2] # StoppedAtFloor [3] } G. Berry, Coll ge de France 21/02/2018 19

  20. Vrification par observateurs (N. Halbwachs) OK Prog Obs BUG E Env Pour toutes les s quences d entr e OK, l observateur n met jamais BUG G. Berry, Coll ge de France 21/02/2018 20

  21. Assertion temporelle : l ascenseur ne voyage pas la porte ouverte signal Running in loop await Start ; abort sustain Running when CabinStopped end loop || loop await OpenDoorMotorOn ; abort sustain assert DoorOpenedWhenMovingBug if Running when DoorIsClosed end loop end signal G. Berry, Coll ge de France 21/02/2018 21

  22. Dfinition de lenvironnement Mais l ascenseur n volue pas dans un environnement physique quelconque ! caract risation de l environnement, indispensable pour v rifier les propri t s et produire des contre-exemples pertinents en r duisant les entr es et l espace d tats La caract risation de l environnement est souvent longue et d licate ! mais elle nous en apprend beaucoup G. Berry, Coll ge de France 21/02/2018 22

  23. Contraintes denvironnement de lascenseur trap Bad in always // no up call button at top floor if UpCall [N-1] then exit Bad end || // no down call button at bottom floor if DownCall [0] then exit Bad end || // elevator is at most at one floor at a time if not ( ReachingFloor [0] # ReachingFloor [1] # ReachingFloor [2] # ReachingFloor [3] ) then exit Bad end if || // A door must be open or closed ( Musset ) if not ( DoorIsOpen # DoorIsClosed ) then exit Bad end if end always peut mieux faire ! G. Berry, Coll ge de France 21/02/2018 23

  24. Contraintes denvironnement de lascenseur || // at most one TimerExpired after StartTimer abort every immediate TimerExpired do exit Bad end when StartTimer ; loop if TimerExpired then exit Bad end; await TimerExpired ; every TimerExpired do exit end each StartTimer || // at most one CabinStopped with one tick to react loop weak abort every immediate CabinStopped do exit Bad end when Stop ; await CabinStopped ; pause end loop G. Berry, Coll ge de France 21/02/2018 24

  25. Contraintes denvironnement de lascenseur || signal ReachingSomeFloor , ShiftedCurrentFloor [N+3] , MovingUp , MovingDown in sustain { for i < N dopar ReachingSomeFloor <= ReachingFloor [i] end for } || // cannot reach a floor between Stop and Start loop weak abort every ReachingSomeFloor do exit Bad end when Start ; await Stop end loop G. Berry, Coll ge de France 21/02/2018 25

  26. Contraintes denvironnement de lascenseur || signal ReachingSomeFloor , ShiftedCurrentFloor [N+3] , MovingUp , MovingDown in || // when at floor i , the next floor is necessarily i+1 or i-1 loop abort sustain { for i < N do ShiftedCurrentFloor [i+1] <= pre( ShiftedCurrentFloor [i+1]) end for } when immediate ReachingSomeFloor ; emit { for i < N do ShiftedCurrentFloor [i +1] <= ReachingFloor [i] end for }; pause end loop G. Berry, Coll ge de France 21/02/2018 26

  27. Contraintes denvironnement de lascenseur || signal ReachingSomeFloor , ShiftedCurrentFloor [N+3] , MovingUp , MovingDown in || loop await Start ; weak abort if case Up do sustain MovingUp case Down do sustain MovingDown default do emit Ignore end if when Stop end loop G. Berry, Coll ge de France 21/02/2018 27

  28. Contraintes denvironnement de lascenseur || signal || emit ShiftedCurrentFloor [2] ; weak abort every immediate ReachingSomeFloor do exit Bad end when Start ; loop await ReachingSomeFloor ; for i<N dopar if ReachingFloor [i] then if MovingUp and not pre(ShiftedCurrentFloor [i]) then exit Bad end if ; if MovingDown and not pre(ShiftedCurrentFloor [i+2]) then exit Bad end if ; end if end for end loop end signal handle Bad do emit Ignore end trap end module G. Berry, Coll ge de France 21/02/2018 28

  29. Agenda 1. La v rification formelle en Esterel 2. Interfacer le code g n r et le simuler G. Berry, Coll ge de France 21/02/2018 29

  30. Comment excuter un programme Esterel En circuits : engendrer du Verilog, utiliser une CAO standard En logiciel : plusieurs mani res quivalentes d engendrer un code C (ou C++, etc.), et plusieurs fa ons de l int grer dans du code plus g n ral principe : d finir des fonctions associ es aux sorties, donner les entr es, appeler la fonction de r action pas de contrainte sp cifique sur quand et comment mais une contrainte absolue : l ex cution du code de la fonction de r action doit tre atomique. en particulier, les valeurs des entr es doivent rester constantes pendant toute la r action G. Berry, Coll ge de France 21/02/2018 30

  31. Exemple pour ABRO void ABRO_O_O () { printf( O emitted\n ); } void main () { ABRO_reset(); // ABRO initialization ABRO(); // empty tick ABRO_I_A(); // input A ABRO_I_B();// input B, same instant ABRO(); // tick, emits O ABRO_I_R(); // input R, reset } BLEU : d finir par l utilisateur MARRON : d fini par le compilateur Esterel G. Berry, Coll ge de France 21/02/2018 31

  32. Simuler un programme Esterel Seule chose d finir : les types et fonctions de donn es Trois types de simulation : textuelle : entr e des signaux au terminal ou par fichier textuelle : tra age optionnel des signaux, variables, etc. graphique : xes, Esterel Studio textuelle : entr es par clics, sorties visuelles animation color e du code source mixte : magn tophone dans les simulateurs graphiques mixte : lisant et crivant les formats textuels Usage : debugging, non-r gression, ex cution des tests engendr s automatiquement, visulalisation des contre-exemples de v rification G. Berry, Coll ge de France 21/02/2018 32

  33. Agenda 1. La v rification formelle en Esterel 2. Interfacer le code g n r et le simuler 3. Exec : contr le d activit s asynchrones G. Berry, Coll ge de France 21/02/2018 33

  34. Linstruction Exec Id e : appeler des fonctions (ou t ches) ex cut es de fa on asynchrone Attendre leur retour pour terminer au sens d Esterel, lors d un instant suivant Les suspendre ou les tuer si l instruction exec est suspendue ou tu e par Esterel suspend, abort, exit, etc. Usage : calculs longs, appels r seaux, mouvements de bras de robots, etc. G. Berry, Coll ge de France 21/02/2018 34

  35. Exemple input A, B, X; return R; var V, W : integer in loop suspend weak abort exec Task (V, W)(?X+1) when B when A end loop end var valeurs et retours par r f rence valeurs r incarnation passer un unique id chaque appel G. Berry, Coll ge de France 21/02/2018 35

  36. Interface bas niveau dExec (Esterel v5) typedef struct { unsigned int start : 1; unsigned int kill : 1 ; unsigned int active : 1 ; unsigned int suspended : 1 ; unsigned int prev_active : 1 ; unsigned int prev_suspended : 1 ; /* to generate suspend / resume */ unsigned int exec_index ; /* unique id in the program */ unsigned int task_exec_index ; /* unique run-time id*/ void (*pStart)() ; /* takes a function as argument */ int (*pRet)() ; /* may take a value as argument */ } __ExecStatus ; G. Berry, Coll ge de France 21/02/2018 36

  37. Interface haut niveau dExec (Esterel v5) #include "exec_status.h" my_start () { ... } my_kill () { ... } my_suspend () { ... } my_resume () { ... } STD_EXEC (R1, REACT, my_start_1, my_kill_1, my_suspend_1, my_resume_1); STD_EXEC (R2, REACT, my_start_2, my_kill_2, my_suspend_2, my_resume_2); /*engendrer automatiquement un STD_EXEC pour chaque t che */ STD_EXEC_FOR_TASK (TASK, REACT, my_start, my_kill, my_suspend, my_resume); Pr cis, mais assez lourd l usage Tr s simplif en HipHop.js (programmation fonctionnelle) G. Berry, Coll ge de France 21/02/2018 37

  38. function execColor(langPair) { return MODULE (IN text, OUT color, OUT trans, OUT error) { EMIT color("red"); AWAIT IMMEDIATE(NOW(text)); PROMISE trans, error translate(langPair, VAL(text)); EMIT color("green"); } } window.onload = function() { hh = require("hiphop"); m = new hh.ReactiveMachine(MODULE (IN text, OUT transEn, OUT colorEn, OUT transNe, OUT colorNe, OUT transEs, OUT colorEs, OUT transSe, OUT colorSe) { LOOPEACH(NOW(text)) { FORK { RUN(execColor("fr|en"), color=colorEn, trans=transEn); } PAR { RUN(execColor("en|fr"), color=colorNe, text=transEn, trans=transNe); } PAR { RUN(execColor("fr|es"), color=colorEs, trans=transEs); } PAR { RUN(execColor("es|fr"), color=colorSe, text=transEs, trans=transSe); } } }, {debuggerName: "debug"}); } } G. Berry, Coll ge de France 21/02/2018 38

Related


More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#