caa a22 4500 477098096 CHVBK 20180405111533.0 cr unu---uuuuu 170330e19960901xx s 000 0 fre 10.1007/BF02997709 doi (NATIONALLICENCE)springer-10.1007/BF02997709 Utilisation de flots de données pour la spécification et la vérification du comportement des systèmes interactifs [Elektronische Daten] [Bruno d'Ausbourg, Guy Durrieu, Pierre Roche] Using flows for describing and verifying the behaviour of interactive systems In some contexts, especially in safety or security critical applications, it may be crucial to verify that the interactive behaviour of these systems possess certain formally expressed properties. Our project is to describe the interactive behaviour of a system by building an abstract formal model of it and to verify automatically that this behaviour possesses the required properties. In this paper, we suggest to use data flows for this purpose. We use the formal language Lustre to denote such flows. This language permits to express safety temporal properties and to build some syntactical structures in order to verify and test them by using appropriate tools. Springer-Verlag, 1996 Interactive system nationallicence Formal description technique nationallicence User interface nationallicence Modeling nationallicence Programming language nationallicence Temporal logic nationallicence Validation nationallicence Système interactif nationallicence Technique description formelle nationallicence Interface utilisateur nationallicence Modélisation nationallicence Langage programmation nationallicence Logique temporelle nationallicence Validation nationallicence d'Ausbourg Bruno onera, 2, avenue E. Belin, BP 4025, F-31055, Toulouse, France aut Durrieu Guy onera, 2, avenue E. Belin, BP 4025, F-31055, Toulouse, France aut Roche Pierre onera, 2, avenue E. Belin, BP 4025, F-31055, Toulouse, France aut Annales Des Télécommunications Springer-Verlag 51/9-10(1996-09-01), 474-482 0003-4347 51:9-10<474 1996 51 12243 https://doi.org/10.1007/BF02997709 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF02997709 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- d'Ausbourg Bruno onera, 2, avenue E. Belin, BP 4025, F-31055, Toulouse, France aut NATIONALLICENCE 700 1- Durrieu Guy onera, 2, avenue E. Belin, BP 4025, F-31055, Toulouse, France aut NATIONALLICENCE 700 1- Roche Pierre onera, 2, avenue E. Belin, BP 4025, F-31055, Toulouse, France aut NATIONALLICENCE 773 0- Annales Des Télécommunications Springer-Verlag 51/9-10(1996-09-01), 474-482 0003-4347 51:9-10<474 1996 51 12243 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer