Publication
Applying model checking to industrial-sized PLC programs
Concepts associés (36)
Supervision (informatique)
La supervision est une technique industrielle de suivi et de pilotage informatique de procédés de fabrication automatisés. La supervision concerne l'acquisition de données (mesures, alarmes, retour d'état de fonctionnement) et des paramètres de commande des processus généralement confiés à des automates programmables. Dans l'informatique, la supervision est la surveillance du bon fonctionnement d’un système ou d’une activité. À ne pas confondre avec l'hypervision, qui elle correspond à la centralisation des outils de supervision, d’infrastructure, d'applications et de référentiels (ex.
Automate programmable industriel
vignette|Deux automates programmables industriels & leurs périphériques, montés en volant, pour test et analyse. Un automate programmable industriel, ou API (en anglais programmable logic controller, PLC), est un dispositif électronique numérique programmable destiné à la commande de processus industriels par un traitement séquentiel. Il envoie des ordres vers les préactionneurs (partie opérative ou PO côté actionneur) à partir de données d’entrées (capteurs) (partie commande ou PC côté capteur), de consignes et d’un programme informatique.
Vérification formelle
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
UML (informatique)
Le Langage de Modélisation Unifié, de l'anglais Unified Modeling Language (UML), est un langage de modélisation graphique à base de pictogrammes conçu comme une méthode normalisée de visualisation dans les domaines du développement logiciel et en conception orientée objet. L'UML est une synthèse de langages de modélisation objet antérieurs : Booch, OMT, OOSE. Principalement issu des travaux de Grady Booch, James Rumbaugh et Ivar Jacobson, UML est à présent un standard adopté par l'Object Management Group (OMG).
Langage de modélisation
Un langage de modélisation est un langage artificiel qui peut être utilisé pour exprimer de l'information ou de la connaissance ou des systèmes dans une structure qui est définie par un ensemble cohérent de règles. Les règles sont utilisées pour l'interprétation de la signification des composants dans la structure. Un langage de modélisation peut être graphique ou textuel.
Automation
L'automation consiste à utiliser les services d'un logiciel dans une application informatique. L'automation peut donc être considérée comme une procédure d'automatisation. En informatique musicale, dans un séquenceur, l'automation consiste à programmer des changements de réglages pendant la lecture d'un morceau, comme la variation de volume d'une piste audio. Cette mise en place peut se faire par mimétisme : le logiciel enregistre en temps réel des mouvements venant de l'utilisateur pour les reproduire lors des prochaines exécutions du morceau.
Stratégie de régulation
Une stratégie (ou topologie) de régulation est, pour un procédé industriel, l'organisation du système de contrôle-commande en vue de maintenir une grandeur physique dans une plage de tolérance donnée. Le choix de stratégie est très important dans les industries de transformation (par exemple les industries chimiques, papetières, agroalimentaires) en raison de la variabilité d'un nombre élevé de grandeurs physiques incidentes (dites « perturbations ») qui y sont présentes.
Système numérique de contrôle-commande
vignette|Deux racks de CS3000, un SNCC de Yokogawa. De droite à gauche, dans le rack supérieur : une alimentation, une CPU, une carte bus pour communiquer avec l'autre rack, des cartes d'entrées-sorties ; dans le rack inférieur : idem sauf la CPU. On peut remarquer que la CPU est connectée à deux câbles Ethernet redondants pour communiquer avec d'autres CPU et des PC de supervision. Un système numérique de contrôle-commande (SNCC, ou DCS pour distributed control system en anglais) est un système de contrôle d'un procédé industriel doté d'une interface homme-machine pour la supervision et d'un réseau de communication numérique.
Méthode formelle (informatique)
En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet).
Contrôle de processus
Le contrôle de processus est un terme utilisé pour désigner l'ensemble du matériel et des logiciels servant à piloter et surveiller le processus de fabrication de produits. Il est le plus souvent constitué d'une chaîne de moyens (appelée boucle de régulation) : capteurs de mesures physiques ou physico-chimiques : pression, niveau, débit, température, pH, viscosité, turbidité, conductivité... Ces capteurs fournissent aux régulateurs de manière continue ou discrète l'indication directe ou indirecte de l'état du processus.