Version du calculateur CLEARSY Safety Plateform à des fins académiques

CLEARSY Safety Plateform académique

La CLEARSY Safety Platform académique est une version simplifiée de la plateforme industrielle permettant de développer et de déployer des applications critiques jusqu’au niveau SIL4. Elle permet de s’initier à la modélisation formelle et à la programmation de contrôle commande de fonctions critiques, dans un cadre juste simplifié pour convenir à une session de formation d’une dizaine d’heures.

La CLEARSY Safety Platform académique est un ordinateur sûr de fonctionnement (la sûreté de fonctionnement fait référence au contrôle des risques reconnus afin d’atteindre un niveau de risque acceptable) capable d’effectuer une auto-évaluation et de vérifier s’il peut accomplir sa mission en toute sûreté. L’auto-évaluation repose sur un certain nombre de caractéristiques matérielles et logicielles pour détecter, par exemple, la corruption de la mémoire, la dérive de l’horloge ou les courants de fuite.

L’architecture principale repose sur 2 microcontrôleurs exécutant le même programme tout en vérifiant régulièrement qu’ils peuvent communiquer entre eux. Les sorties numériques sont des relais électriques nécessitant que les deux microcontrôleurs soient d’accord pour s’activer. Si l’auto-évaluation échoue, l’ordinateur désactive ses sorties et entre dans une boucle infinie ne faisant rien. Le programme exécuté se compose de deux parties :

• une partie développée en langage C et assembleur MIPS, appelée code non répliqué, contenant la boucle principale, le traitement des interruptions et certaines fonctions non liées à la sécurité.
• une partie développée avec B (spécification et implémentation), appelée code répliqué, qui contient l’application critique.

Les codes binaires sont produits à partir de l’implémentation B en utilisant deux générateurs de code différents (C + gcc d’une part, compilateur maison de B vers binaire d’autre part). À chaque itération de la boucle principale, les deux binaires sont exécutés en séquence et leurs espaces mémoire contenant les variables de sûreté doivent avoir exactement le même contenu. Les vérifications sont programmées une fois pour toutes dans la bibliothèque de sûreté fournie avec l’Atelier B. Les propriétés de sûreté de la plateforme sont hors de portée du développeur qui ne peut pas les altérer.

La CLEARSY Safety Platform académique se compose d’un calculateur de dimensions réduites (10cm x 10cm x 2cm), doté respectivement de 3 entrées et 2 sorties numériques, embarquant deux micro contrôleurs PIC32, ainsi que d’un environnement de développement intégré basé sur l’ Atelier B.

Le logiciel, le code non répliqué en C et la bibliothèque de sécurité sont fournis sous une forme non modifiable. Le développeur n’a qu’à modifier le projet B fourni afin de spécifier et d’implémenter la fonction de contrôle des sorties en fonction de l’état des entrées. Afin de maintenir le prix d’achat à un niveau acceptable pour un établissement universitaire, le calculateur n’embarque pas toute l’électronique sécuritaire de la version industrielle. Cette carte ne peut donc pas être utilisée dans un système critique de sécurité réel.

Téléchargements

• Télécharger la documentation
• Télécharger l’environnement de développement intégré (IDE)

Dissémination

La CLEARSY Safety Platform est utilisée comme support de formation pour l’enseignement des méthodes formelles principalement en dernière année de cursus universitaire, en Europe et en Amérique. Parmi les utilisateurs, on mentionnera l’université de Louvain (Belgique), l’université Fédérale du Rio Grande du Nord (Brésil), l’université de Sherbrooke (Canada), l’université de Florence (Italie), l’université de Swansee (Royaume Uni), ainsi que l’université Aix-Marseille, CentraSupélec, l’ENSIIE, l’ESIEE, Eurecom, l’université Paris-Dauphine, Telecom Paris, l’UPEC en France.

Configurations

La CLEARSY Safety Platform existe en 2 configurations pour un usage académique et de démonstration :

Carte SK0 simple

Cette carte, entièrement fonctionnelle, est dotée de 2 processeurs PIC32MX795F512L, de 512 Ko de Flash et de 128 Ko de RAM. Elle comprend 3 entrées et 2 sorties binaires. Elle se programme en B avec l’Atelier CLEARSY Safety Platform.

Carte SK0 avec accessoires

Idéale pour une mise en œuvre immédiate. Elle comprend :

• 1 carte SK0 assemblée (plexiglass avec sérigraphie, entretoises),
• 1 alimentation 5V,
• 1 câble micro USB,
• 3 interrupteurs

Prix de vente de la carte SK0

Quantités	x1	x10
carte SK0 simple	275€ HT	2 500€ HT
carte SK0 avec accessoires	325€ HT	2 900€ HT

Les frais de port sont en sus. Ils s’établissent à 50€ pour une commande de 1 ou 10 cartes pour toute destination en Europe. Pour d’autres quantités ou destinations, veuillez nous consulter.

Chaque carte SK0 est fournie avec :

• sa documentation au format électronique (PDF),
• l’environnement de développement logiciel (Atelier CLEARSY Safety Platform). Il comprend un atelier de modélisation formelle en langage B, une double chaine de compilation et un utilitaire de chargement des programmes dans la carte SK0. L’environnement nécessite un système d’exploitation Windows récent.

Nos produits CLEARSY Safety Platform sont entièrement fabriqués en France.

Choisir une configuration* SK0 simple SK0 avec accessoires

Choisir la quantité* 1 10

J'autorise CLEARSY à collecter mon nom et mon adresse email en vue de pouvoir me répondre. Pour plus d'informations, consultez notre politique de confidentialité.

J'accepte de recevoir la lettre d'information CLEARSY par email.