Formalisation en vue de la vérification de propriétés du langage à blocs fonctionnels IEC 61499
Institution:
Cachan, Ecole normale supérieureDisciplines:
Directors:
Abstract EN:
"The IEC 61499 standard's draft propose a function blocks language for industrials-process measurement and control systems. The goal of this language is , in a implementation view, to allow the specification of distributed and complex systems. But, one can reproach to this standard not to give a formal enough definition of the language so tha all the fonction blocks diagrams built with the standard can be described without ambiguity or can be validated. The aim of our work is double : first we must formally define the standard's language in a static view in order to establish a coherent discourse universe; and we'll give a dynamic behavior interpretation for the block and the blocks diagram. Those definitions, in a static metamodeling and in a behavior modeling shape will allow us to give a formal and unique syntax and a behavior for the function blocks language. Once this step crossed, we can use these results for the properties verification. In this goal, we first establish a translation method for each steps of the behavior modelong of the function block thanks to a synchronous language (SIGNAL), whith language can be used with properties verification methods. Secondly, we will introduce a temporal frame with different clocks allowing us to guarantee the reactivity aspect for the blocks diagram. Thirdly, thanks to toe temporal frame, we will extend our translation method to the function blocks diagram. We now have a translation method for a function blocks diagram built with the IEC 61499 standard in SIGNAL, we can, thus, use model-checking tools (such as SILDEX) in order to verify some properties in these models. This properties verification method had been used in the steam-boiler example and thanks to it, we were to detect errors an correct them"
Abstract FR:
"Le projet de norme IEC 61499 propose un langage à blocs fonctionnels permettant la description des systèmes de mesure et de contrôle des processus industriels. Ce langage a pour but de permettre la spécification, en vue d'une implantation, de système complexes et distribués. Cependant, on peut reprocher à cette norme de ne pas définir de manière suffisamment formelle ce langage pour que tout réseau de blocs fonctionnels conforme à la norme IEC 61499 soit sans ambiguïté et puisse être validé. L'objectif de notre travail est donc double puisqu'il nous faudra tout d'abord définir formellement le langage de la norme de manière statique afin d'établir un univers du discours cohérent; puis nous donnerons une interprétation dynamique du comportement du bloc et du réseau de blocs. Ces définitions, sous la forme d'un métamodèle statique et de la modélisation du comportement, nous permettent d'établir une syntaxe et un comportement formels et univoques du langage à blocs fonctionnels. Une fois cette étape effectuée, nous pouvons utiliser ces résultats dans une optique de vérification de propriétés. Pour ce faire, nous établissons tout d'abord une méthode de traduction de chacune des différentes étapes de la modélisation du comportement du bloc fonctionnel à l'aide du langage synchrone SIGNAL pouvant être utilisé avec des logiciels de vérification de propriétés. Puis nous introduisons un cadre temporel à différentes échelles de temps permettant d'assurer la réactivité du réseau de blocs fonctionnels. Enfin, nous étendons notre méthode de traduction au réseau de bloc à l'aide de ce cadre temporel. Nous obtenons ainsi une méthode de traduction d'un réseau de blocs fonctionnels conforme à la norme IEC 61499 en langage SIGNAL. Il est alors possible d'utiliser des outils de model-checking tels que SILDEX pour faire de la vérification de propriétés sur ces modèles. Cette méthode de vérification de propriétés a été appliquée à un exemple (le générateur de vapeur) et nous a permis de détecter des erreurs et de les corriger"