30
F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 1 Introduction à SCADE ®

Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

Embed Size (px)

Citation preview

Page 1: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 1

Introduction à SCADE®

Page 2: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 2

Introduction

SCADESCADE : : SSafety-afety-CCritical ritical AApplicationpplication D Development evelopment EEnvironmentnvironment● environnement de développement pour les systèmes

critiques, en particulier dans le domaine de l’embarqué➢ avionique (Airbus, Eurocopter) : leader de facto➢ nucléaire (Schneider Electrics, CEA) ➢ automobile (standard émergent)

● développé initialement par le laboratoire Verimag de Grenoble à partir des travaux de recherche avec Lustre

● maintenant commercialisé par la société Esterel Technologies

Page 3: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 3

Historique

Esterel TechnologiesEsterel Technologies● en 1984, premiers éléments du langage Esterel (issu des

travaux pour construire un robot mobile pour un concours organisé par une revue de microélectronique)

● groupe de recherche autour de Gérard Berry pour le développement d’Esterel

➢ utilisation du langage par des sociétés (AT&T Bell Labs, Bertin, Dassault)

● V4 du compilateur Esterel en 1994➢ implémentation des programmes sur des FPGA, ou par soft

● en 1997, intégration du langage graphique SyncCharts (proche des StateCharts)

➢ utilisé par Dassault, Thales, Thomson CSF➢ logiciel Esterel Studio, développé par Simulog➢ en 1999, création de Esterel Technologies

Page 4: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 4

Historique

SCADESCADE● Lustre développé dans les années 1980 (P. Caspi, N.

Halbwachs, laboratoire IMAG)● en 1986, utilisé par Merlin Gérin (maintenant Scheider

Electric) pour le contrôle des centrales nucléaires (outil Saga)

➢ développement avec Verilog● rapprochement avec Aérospatiale (maintenant Airbus) qui

utilise un outil analogue (SAO)● Verilog, en partenariat avec Merlin Gérin et Aérospatiale,

développe un outil commun : SCADE● en 1993, Verilog et IMAG créent un laboratoire commun :

Verimag● SCADE racheté par Telelogic en 1999, puis par Esterel

Technologies en 2001● en 2015, Esterel Technologies racheté par ANSYS

Page 5: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 5

SCADE aujourd’hui● environnement de développement basé sur Lustre et

Esterel➢ le langage textuel de SCADE est basé sur Lustre V3➢ utilisé pour sauvegarder les modèles (fichiers .saofd)

● ESTEREL SCADE SuiteTM est le standard pour la création d’applications critiques embarquées

➢ qualifié pour le standard DO-178B/ED-12B (niveau A) pour l’avionique et les applications militaires

➢ certifié pour le standard IEC 6158 (niveau 3) pour les équipements lourds et la production d’énergie

➢ conforme au standard EN 60128 (niveau 3/4) pour les applications ferroviaires

➢ compatible avec le standard IEC 60880 pour le nucléaire● associé maintenant à ESTEREL SCADE DisplayTM , un

environnement de développement graphique pour concevoir et vérifier des applications telles que les systèmes d’affichage de cockpit ou de tableaux de bord

Page 6: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 6

Standard DO-178B/ED-12B

● document produit par la RTCA (DO-178B, USA) et EUROCAE (ED-12B, Europe) pour fournir des lignes directrices précisant la façon de produire du code pour les applications aéronautiques (1ère version en 1992)

➢ complémentaire du document ARP 4754 qui spécifie le processus de conception des systèmes de pilotage et de modification des systèmes existants

System life-cycle processes (ARP 4754)System safety assessment process

Software life-cycle processes (DO-178B)part of implementation processees, for ARP 4754

System requirementsallocated to software

Software level(s)

Design constraintsHardware definitions

Fault containmentboundaries

Error sourcesidentified/eliminated

Software requirements& architecture

Page 7: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 7

● les lignes directrices spécifient :➢ les objectifs pour chaque phase du cycle de vie du code➢ la description des activités et des considérations quant à la

conception pour atteindre ces objectifs➢ la description des preuves montrant que ces objectifs ont

été atteints

Standard DO-178B/ED-12B

Page 8: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 8

Standard DO-178B/ED-12B

● DO-178B et ARP 4654 définissent en commun les niveaux de criticité pour les systèmes, leurs composants et le code :

➢ Niveau A : Problème catastrophique - Sécurité du vol ou atterrissage compromis - Crash de l'avion

➢ Niveau B : Problème majeur entraînant des dégâts sérieux voire la mort de quelques occupants

➢ Niveau C : Problème sérieux entraînant un dysfonctionnement des équipements vitaux de l'appareil

➢ Niveau D : Problème pouvant perturber la sécurité du vol➢ Niveau E : Problème sans effet sur la sécurité du vol

● l’approche est orientée objectif : on formule les objectifs et on vérifie qu’ils ont été atteints

➢ mais les méthodes précises à utiliser ne dont pas données (le cycle de vie du développement n’est même pas spécifié)

Page 9: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 9

Standard DO-178B/ED-12B

● approche proposée par DO-178B :➢ s’assurer que les objectifs appropriés sont définis, e.g.

✔ niveau de criticité du développement du code✔ standards de conception

➢ définir des procédures pour la vérification des objectifs, e.g.

✔ vérifier que l’indépendance des activités correspond au niveau de criticité du développement

✔ vérifier que les standards de conception sont satisfaits et que la conception est complète, précise et traçable

➢ définir des procédures pour vérifier que les procédures de vérification précédemment définies sont exécutées correctement, e.g.

✔ vérifier que les remarques des revues des documents de conception ont bien été prises en compte

✔ vérifier que les tests montrant que le contenu du cahier des charges est rempli ont été effectués

Page 10: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 10

L’outil SCADE

● la satisfaction du standard est très contraignante pour les développeurs (« rendement » en termes de lignes de code produites par jour typiquement 4 fois plus faible que pour des applications non critiques

● des outils pour aider à satisfaire le standard sont essentiels

● fournit l’ensemble des fonctionnalités réclamées par les standards pour le codage d’applications critiques :

➢ modélisation de l’application➢ vérification du modèle➢ génération de code certifié

Page 11: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 11

modélisation de l’application

● architecture typique d’un système temps réel embarqué critique :

Contrôleur

Gestion des entrées-sorties

Systèmed’exploitation

Pilotes

Matériel

composantsde bas niveau

composantsde bas niveau

gestion des données

gestion des données

applicationinteragissant

avec

applicationinteragissant

avec

environnementenvironnement

lois de contrôle,algorithmes,

logique d’accès aux « modes »,etc...co

mpl

exe

!

Page 12: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 12

● SCADE propose un langage rigoureux pour saisir les besoins en matière de calcul et de logique

➢ équations de flot de données pour le calcul➢ machines à états pour la logique

➢ la fonction principale de SCADE est appeléede façon cyclique

➢ code développémanuellement pourl’interfaçage avec les couches logicielles debas niveau et le matériel

modélisation de l’application

Lustre

Esterel

Gestion des entrées-sorties

Systèmed’exploitation Pilotes

Matériel

Contrôleur

Fonction SCADE

Co

de

man

uel

Co

de

man

uel

Page 13: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 13

Modélisation avec SCADE

● utilise 2 formalismes de spécifications :➢ des machines à états finis pour les modes de

fonctionnement et les transitions➢ des diagrammes de flots de données pour les algorithmes

de contrôle● s'appuie sur ESTEREL et LUSTRE

● Les illustrations qui suivent proviennent du manuel

Page 14: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 14

Modélisation avec SCADE

● les blocs de base sont les "opérateurs"➢ représentés graphiquement

➢ ou textuellement

➢ pré-définis dans le langage➢ ou définis par l'utilisateur à l'aide d'opérateurs

✔ permet de construire des structures très complexes

Page 15: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 15

Modélisation avec SCADE

● diagrammes de flots de données pour les contrôles continus

➢ traitements périodiques du signal● opérateurs entre lesquels circulent des flots de données

● les opérateurs sont ➢ modulaires (comportement indépendant du contexte)➢ fortement typés

✔ chaque donnée a un type✔ la cohérence des types est vérifiée

Page 16: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 16

Modélisation avec SCADE

● SCADE permet de vérifier les timings et la causalité➢ circuits récursifs➢ exemple

délai avecvaleur initiale

Page 17: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 17

Modélisation avec SCADE

● SCADE permet de vérifier que les flots de données sont initialisés correctement (essentiel dans le développement d'applications critiques)

Page 18: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 18

Modélisation avec SCADE

● les contrôles « discrets » permettent de réagir aux événements externes asynchrones

➢ alarmes➢ capteurs « discrets »➢ interfaces homme-machine

● modélisés par des machines à états finis● incluant des opérateurs de flots de données

Page 19: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 19

Modélisation avec SCADE

● modèle de calcul basé sur une boucle

➢ calcul non interruptible dès que les capteurs ont été lus➢ tous les opérateurs ont une horloge basée sur une horloge

maître (cf Lustre)➢ les machines à états finis utilisent aussi une approche

cyclique✔ passage d'événements entre machines✔ communication entre machines et opérateurs

● l'identité des comportements du modèle séquentiel généré et des spécifications initiales est garanti par des méthodes formelles

Page 20: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 20

vérification du modèle

● but de la vérification :➢ conformité du modèle établi avec les spécifications

contenues dans le cahier des charges➢ absence de fonctions non intentionnelles, sans rapport avec

le contenu du cahier des charges● plusieurs phases dans le processus de vérification

➢ revue du modèle➢ simulation➢ couverture structurelle➢ vérification formelle➢ prédiction des performances

● à chaque étape, SCADE fournit des outils spécifiques

Page 21: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 21

vérification du modèle

● revue du modèle➢ vérification que chaque élément d’un modèle SCADE est en

rapport direct avec une ou plusieurs exigences fournies en entrée de la phase de conception du modèle

➢ l’outil « SCADE Suite Requirements Management GatewayTM » gère la traçabilité des exigences à travers SCADE

➢ calcule également le pourcentage de couverture des exigences par le modèle

Page 22: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 22

vérification du modèle

● simulation➢ vérification fonctionnelle à l’aide de l’outil « SCADE Suite

SimulatorTM »➢ SCADE garantit que les résultats de la simulation du

modèle sont identiques à ceux qui seront obtenus plus tard par le code généré à partir du modèle sur la cible

➢ outil complémentaire « SCADE Suite Rapid PrototyperTM »

Page 23: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 23

vérification du modèle

● couverture structurelle➢ mesure de combien ce logiciel a été testé➢ permet d’identifier des parties de ce logiciel qui n’ont jamais

est testées➢ outil « SCADE Suite Model Test CoverageTM » (requis par

les normes comme DO-178B ou EN-50128)➢ peut mettre en évidence

✔ les éventuelles insuffisances des tests✔ des contradictions dans les exigences ou des parties du

modèle qui ne sont pas accessibles, et qui sont donc inutiles

Page 24: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 24

vérification du modèle

● développement « traditionnel »

Page 25: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 25

vérification du modèle

● développement « SCADE »

Page 26: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 26

vérification du modèle

● vérification formelle➢ vient en complément des tests de simulation

✔ avec les tests, on ne peut pas être sûr à 100% que le modèle est correct (il peut manquer des scénarios d’exécution dans l’ensemble des tests)

➢ utilise l’outil « SCADE Suite Design VerifierTM » associé au plugin Prover Plug-InTM de Prover TechnologyTM (analogue à LESAR dans Lustre)

✔ l’utilisateur fournit un ensemble de propriétés de sûreté qui doivent être vérifiées (décrites dans le formalisme de SCADE)

✔ Design Verifier effectue une analyse mathématique et exhaustive de l’ensemble des comportements possibles du système

✔ si la propriété n’est pas vérifiée par un des scénarios, Design Verifier fournit un point de départ pour une nouvelle simulation conduisant à une erreur, qui peut alors être plus facilement corrigée

Page 27: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 27

vérification du modèle

● prédiction des performances➢ utilise l’outil « SCADE Suite Timing and Stack VerifierTM » ➢ pour le code qui sera généré pour la cible, donne

✔ une estimation du temps d’exécution maximal du code C✔ sa consommation maximale d’espace mémoire sur la pile

➢ intègre une technique d’analyse statique développée par Absint avec l’outil aiT

✔ repose à la fois sur le modèle SCADE de l’application et sur un modèle du processeur cible qui permettra d’évaluer les performances

Page 28: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 28

génération de code certifié

● la phase de codage suivant la conception est entièrement automatisée

● utilise le générateur de code certifié « SCADE Suite KCGTM »

● le code produit est➢ traçable par rapport au modèle fourni en entrée➢ lisible➢ conforme à la norme ISO-C➢ indépendant de la cible➢ comportement déterministe

✔ pas d’allocation dynamique de mémoire✔ pas d’opérations arithmétiques sur les pointeurs

● KCG a été développé avec le même niveau d’exigence que celui attendu pour le code produit

➢ certifié niveau A de DO-178B➢ pas de nouvelle vérification nécessaire au niveau du code

Page 29: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 29

Conclusion

● l'utilisation de SCADE permet➢ de réduire de moitié les coûts de certification➢ de réduire de 70% à 90% les coûts de développement,

certification et tests➢ *de réduire de 65% à 75% le temps de mise au point d'un

logiciel➢ de supprimer les erreurs de codage et les tests unitaires

● maintenant le standard de facto de l'avionique

Page 30: Introduction à SCADEfrancois.touchard.perso.luminy.univ-amu.fr/INFO5/Langages/C3-SCADE… · Historique Esterel Technologies ... (proche des StateCharts)

F. Touchard Polytech Marseille Département d'Informatique SyCA 5ème année 2017-18 30

présentation du TD