Search

Your search keyword '"Frédéric Boniol"' showing total 3 results
Start Over Author "Frédéric Boniol" Publisher lavoisier
3 results on '"Frédéric Boniol"'

1. étude de réseaux de Thomas par validation de propriétés LTL pour Pseudomonas aeruginosa

Author

Rémy Wyss, Julien Forget, Claire Pagetti, and Frédéric Boniol

Abstract

Les systemes temps reel critiques doivent souvent repondre a des exigences temporelles de bout en bout, exprimees au niveau modele, mais qui ne sont pour la plupart verifiees qu’au niveau de l’implantation. Cet article se focalise sur trois exigences : la latence d’une entree vers une sortie, la fraicheur d’une sortie relativement a une entree, et enfin la reactivite du systeme vis-a-vis d’une entree. Nous montrons que, en utilisant une approche synchrone enrichie par des horloges temps reel pour la modelisation du systeme, il est possible de calculer ces proprietes automatiquement en faisant abstraction des choix d’implantation.

Published
2015
Full Text
View/download PDF

2. Formalisation de contextes et d’exigences pour la validation formelle de logiciels embarqués

Author

Yves Le Traon, Amine Raji, Beno It Baudry, Jean-Charles Roger, Philippe Dhaussy, Frédéric Boniol, Lab-STICC_ENSTAB_CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) (Lab-STICC), Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Télécom Bretagne-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Télécom Bretagne-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), ONERA - The French Aerospace Lab [Toulouse], ONERA, Ecole Nationale Supérieure d'Electrotechnique, d'Electronique, d'Informatique, d'Hydraulique et de Télécommunications (ENSEEIHT), Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées, Département STIC [Brest] (STIC), École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne), Département Logique des Usages, Sciences sociales et Sciences de l'Information (LUSSI), Université européenne de Bretagne - European University of Brittany (UEB)-Télécom Bretagne-Institut Mines-Télécom [Paris] (IMT), Computer Science and Communications Research Unit [Luxembourg] (CSC), Laboratory of Advanced Software SYstems [Luxembourg] (LASSY), Université du Luxembourg (Uni.lu)-Université du Luxembourg (Uni.lu), Reliable and efficient component based software engineering (TRISKELL), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Université de Toulouse (UT)-Université de Toulouse (UT), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique

Subjects
Computer science [C05] [Engineering, computing & technology], [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], modèles de contexte, 020207 software engineering, 02 engineering and technology, Sciences informatiques [C05] [Ingénierie, informatique & technologie], vérification, scénarios, automates temporisés, patrons de propriétés, exigences formelles, observateurs, cas d'utilisation, Contextes de preuve, 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, 020201 artificial intelligence & image processing, contexte
Abstract

International audience; Un des défis posés aux méthodes formelles est leur intégration dans les processus de développement industriel. Une des difficultés rencontrées par les techniques formelles telles que le model-checking est l'explosion de l'espace des états à explorer lors de la vérification. Pour réduire cet espace des états, il est nécessaire de décrire le comportement de l'environnement qui est en interaction avec le système à valider. Cet article s'intéresse à la formalisation de cet environnement que nous nommons " contexte " en lien avec la formalisation des propriétés. Dans ce but, nous proposons et expérimentons un DSL, nommé CDL (Context Description Language) reposant d'une part sur des diagrammes d'activités et de séquences pour l'expression du comportement de l'environnement, et d'autre part sur la notion d'observateur pour l'expression des propriétés à vérifier. Afin de contourner l'explosion des états produite par la composition des modèles de l'environnement et du système à valider, nous appliquons une technique de partitionnement du comportement de l'environnement en sous-contextes analysables séparément. Nous illustrons notre contribution par un exemple, et présentons les retours d'expérience obtenus sur six cas d'études industriels.

Published
2012
Full Text
View/download PDF

3. Trois approches pour la modélisation et la vérification de systèmes embarqués

Author

Frédéric Boniol, Gérard Bel, and Jérôme Ermont

Abstract

L'objectif de cet article est de montrer la faisabilite de la verification formelle de proprietes mixtes fonctionnelles et temps reel sur un systeme embarque. Trois approches sont developpees. Une premiere comparaison oppose d'une part une technique operant sur un modele de temps continu (le verifieur UPPAAL associe aux automates temporises) a des techniques operant sur des modeles de temps discrets. Parmi ces dernieres, une seconde comparaison oppose les techniques de « model checking », illustrees ici par le verifieur SMV associe au langage LUSTRE, a des techniques plus couramment utilisees dans le domaine de l'optimisation combinatoire, illustrees dans cet article par une methode de satisfaction de contraintes. Ces comparaisons, realisees sur un exemple du monde avionique, contribuent a montrer la robustesse des approches par contraintes face au phenomene de l'explosion combinatoire.

Published
2003
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results