- Contrôle d'un atelier flexible - Cet exemple présente une méthode pour spécifier, vérifier et implémenter un contrôleur pour une cellule de production robotique en utilisant l'approche Signal. Ce travail a été réalisé dans le cadre d'une étude de cas concernant une cellule de production, proposée par le FZI de Karlsruhe. La spécification est structurée de façon modulaire, en utilisant deux principes de décomposition: l'un suivant l'architecture de la cellule de production, l'autre séparant clairement le modèle du système et son contrôleur. Ce dernier point est une originalité de l'approche, comparée aux approches impératives: le language déclaratif est utilisé pour spécifier, sous forme d'équations sur des signaux, les comportements possibles d'un système, et un contrôleur les contraignant. De cette façon, on peut construire des hiérarchies de systèmes contrôlés imbriqués : dans le cas de la cellule de production, le comportement ordonnancé est une instance contrôlée du comportement sûr, qui est lui même une instance contrôlée du comportement naturel. Le modèle de la cellule de production est fait en termes d'événements et de booléens. S'abstraire ainsi de la nature numérique de certains capteurs permet l'analyse formelle de propriétés du système. Le caractère équationnel de Signal mène naturellement à l'utilisation de méthodes fondées sur les systèmes polynomiaux dynamiques d'équations sur ZZ=3ZZ pour la preuve formelle de la satisfaction des propriétés nécessaires à l'application. Processus Signal décrivant le contrôleur (Cliquez pour agrandir) Processus Signal décrivant la presse (Cliquez pour agrandir)