AFSEC

Approches Formelles des Systèmes Embarqués Communicants

Archive pour la catégorie 'Actions Afsec'

MOVEP 2014, 7-11 July 2014, Nantes, France

Sunday 4 May 2014

11th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2014), 7-11 July 2014, Nantes, France.

MOVEP 2014 is supported by AFSEC.

Program

MOVEP is a 5 day summer school about modeling and verifying parallel processes. The first five occurrences of the School took place in Nantes (France) every other year from 1994 to 2002. It then moved to Brussels (Belgium) in 2004 Bordeaux (France) in 2006, Orléans (France) in 2008, Aachen (Germany) in 2010, and Marseilles (France) in 2012.

For the 20th anniversary of the event, the 11th edition will be held once again in Nantes.

General topics relate to specification and verification of computerized systems designed for the control of real-time applications, reactive or critical systems, and involving concurrent processes.

The purpose of MOVEP is to bring together researchers, students and people from industry working in the fields of control and verification of concurrent and reactive systems. The School seeks to offer a broad spectrum of current research in this area of theoretical and applied computer science. The topics covered by MOVEP’14 include model-checking, controller synthesis, software verification, temporal logics, real-time and hybrid systems, stochastic systems, security, run-time verification, etc.

The Program of the School consists of six 2h30 tutorials and five 1h30 technical talks.

Publié dans Actions Afsec, Ecoles d'été | Pas de commentaire »

Programme du workshop AFSEC lors des journées GPL

Saturday 8 March 2014

Le Workshop AFSEC se tiendra le vendredi 13 juin (session 11h-12h30) lors des journées nationales du GDR GPL qui se dérouleront du 11 au 13 juin 2014 au Cnam à Paris
Elles seront co-localisées avec CAL, CIEL et AFADL : http://cedric.cnam.fr/cpr/gdr-gpl2014/ .

Programme du Workshop AFSEC :

  • Marc Pouzet (Ecole Normale Supérieure, Paris.)
    Une analyse des boucles de causalite dans les modeleurs de systemes hybrides.
  • Resume: Les modeleurs de systemes hybrides tels que Simulink/Stateflow permettent de decrire des systemes a temps discret et continu. Un des points delicats de leur compilation est le traitement des boucles de causalite. Dans cet expose, nous presenterons une analyse de ces boucles pour un langage combinant des constructions d’un langage synchrone — equations de suites, automates hiérarchiques et composition parallele synchrone — et des equations differentielles ordinaires (ODEs). Nous illustrerons cette analyse a l’aide d’exemples écrits en Zélus (zelus.di.ens.fr). Il s’agit d’un travail en commun avec Albert Benveniste, Timothy Bourke, Benoit Caillaud et Bruno Pagano.

  • Étienne André (LIPN, Paris 13)
    Analyse de robustesse précise pour réseaux de Petri temporels
  • Résumé: Quantifier la robustesse des systèmes temporisés consiste à mesurer l’extension maximale des constantes temporelles du système tel que celui-ci satisfasse toujours sa spécification. Ici, nous introduisons une notion de robustesse précise, considérant une mesure locale de la variabilité de toutes les constantes temporelles. Nous considérons cette étude dans le formalisme des réseaux de Petri temporels à arcs inhibiteurs. Nous utilisons la méthode inverse, définie à l’origine pour les automates temporisés, ce qui nous permet d’exprimer cette mesure de robustesse sous la forme d’une contrainte portant sur les différentes constantes du système. Nous proposons aussi une technique afin de rendre robuste un système qui ne l’était pas. Il s’agit d’un travail en commun avec Giuseppe Pellegrino, Laure Petrucci

  • Julien Tanguy (SeeForSys, IRCCyN)
    Synthèse de pilotes de périphériques pour systèmes temps-réel embarqués
  • Résumé: Le développement logiciel de systèmes embarqués critiques (avec des contraintes de temps-réel, de sûreté) est une tâche complexe et difficile.
    A la base de tous les systèmes embarqués, les pilotes doivent prendre en compte un très grand nombre de cas d’utilisations grâce à une généricité et une configurabilité toujours plus grande.
    Des erreurs de configuration peuvent entrainer des bugs graves, cependant l’analyse de toutes les configurations possibles est une tâche difficile.
    Nous proposons une méthode alternative qui est de synthétiser entièrement les pilotes de périphérique grâce aux méthodes formelles.
    A partir de la modélisation du périphérique et de son environnement d’exécution (application, OS, etc.), il est possible de synthétiser un modèle du pilote répondant par construction à des propriétés temporelles, fonctionnelles et de sécurité.
    Ce modèle du pilote est ensuite transformé en code afin d’être embarqué pour une application donnée.
    En déplaçant la configuration au niveau modèle, on simplifie la vérification du code embarqué, et on bénéficie d’outils puissants de model-checking afin de vérifier les contraintes fonctionnelles et de sûreté de fonctionnement.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Workshop AFSEC

Tuesday 28 January 2014

Comme chaque année, l’action AFSEC est invitée à organiser une session lors des journées nationales du GDR GPL qui se dérouleront du 11 au 13 juin 2014 à Paris.
Elles seront co-localisées avec CAL, CIEL et AFADL (http://cedric.cnam.fr/cpr/gdr-gpl2014/).

Si vous souhaitez faire un exposé de vos travaux dans le cadre de la session AFSEC de ces journées, merci de faire parvenir par email (à Olivier H Roux) un titre et un résumé de votre présentation.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Les diapos des présentations de la journée AFSEC concurrence du 19 novembre 2013

Friday 22 November 2013

Publié dans Actions Afsec, Journées | Pas de commentaire »

Journée AFSEC concurrence le 19 novembre 2013 à Cachan

Wednesday 10 July 2013

Une journée sur le thème de la concurrence se tiendra le 19 novembre 2013 à l’ENS Cachan.

Lieu : salle 102
Accès : entrer dans le bâtiment d’Alembert par le haut du fer à cheval, monter un étage, aller à gauche et encore à gauche (on se retrouve en fait au-dessus des bureaux du LSV)

Programme :

10h15

  • Accueil - café

10h45 - 12h00

  • Benedikt Bollig (LSV, CNRS, ENS Cachan)
    Logic for Communicating Automata with Parameterized Topology
  • Didier Lime (IRCCyN, École Centrale de Nantes)
    Dépliage symbolique des réseaux de Petri temporels

12h00 - 13h45

  • Déjeuner

13h45 - 15h00

  • Rémi Morin (LIF, Université d’Aix-Marseille)
    Vérification de MSG à l’aide d’outils
  • Yann Thierry-Mieg (LIP6, Université Pierre & Marie Curie, Paris)
    Expressing concurrent system semantics with GAL

15h30 - 16h45

  • Loïc Paulevé
    Interpretation of Traces for Asynchronous Automata Networks
  • Bernard Berthomieu (LAAS, CNRS, Toulouse)
    Specifying and verifying real time systems with Fiacre/Tina

Contact : Thomas Chatain

Publié dans Actions Afsec, Journées | Pas de commentaire »

Ecole d’été temps réel ETR 2013 (du 26 au 30 août 2013)

Monday 17 June 2013

La huitième école d’été temps-réel ETR 2013 (http://www.irit.fr/ETR13//)
aura lieu à l’ENSEEIHT, Toulouse.
ETR 2013 est soutenue par l’AFSEC.

Les systèmes temps réel sont caractérisés par la nécessité de respecter des contraintes temporelles imposées au système informatique par son environnement. Par exemple, un procédé de fabrication, un avion, un train, un système de surveillance ou un système multimédia sont des exemples de systèmes temps réel. Étant donnée la nature critique des domaines d’application des systèmes temps réel et embarqués, le développement de tels systèmes requiert la mise en œuvre d’approches et de technologies de haut niveau.

Publié dans Actions Afsec, Ecoles d'été | Pas de commentaire »

Modélisation des Systèmes Réactifs (MSR’13)

Sunday 2 June 2013

Colloque Francophone sur la Modélisation des Systèmes Réactifs
Soutenu par l’AFSEC.

INRIA Rennes - Bretagne Atlantique, France, du 13 au 15 novembre 2013

Site : MSR’13

Publié dans Actions Afsec, Conférences | Pas de commentaire »

Workshop AFSEC le 04 avril 2013 à Nancy

Monday 11 February 2013

Workshop AFSEC le 04 avril 2013 à Nancy
lors des journées du GDR GPL du 2 au 5 avril 2013 à Nancy colocalisées avec CIEL et AFADL.

Pdf du programme avec resumés

Programme :

  • Benoît Barbot (LSV, ENS Cachan), Marco Beccuti (Univ. Torino), G. Franceschinis (Univ. Piemonte Orientale) et Serge Haddad (LSV, ENS Cachan)
    “Partially Observed Markov Decision Process, for Energy Management in Wireless Sensor Networks”
  • Frédéric Boniol et Virginie Wiels (ONERA Toulouse)
    “Ingénierie formelle pour logiciels aéronautiques certifiés.”
  • Sylvain Cotard, Sebastion Faucou et Jean-Luc Bechennec, (Renault & IRCCyN Nantes)
    “Runtime Verification for Real-Time Automotive Embedded Software”
  • Iulia Dragomir, Iulian Ober, Christian Percebois (IRIT TOULOUSE)
    “Contrats pour composants réactifs temporisés”

Publié dans Actions Afsec, Journées | Pas de commentaire »

Workshop AFSEC 2013 lors des journées GPL - Appel à communication

Friday 1 February 2013

Comme chaque année, l’action AFSEC est invitée à organiser un workshop lors des journées nationales du GDR GPL qui se dérouleront du 2 au 5 avril 2013 à Nancy.
Ces journées seront colocalisées avec CIEL et AFADL.

Le workshop AFSEC se tiendra le jeudi 4 avril

Si vous souhaitez faire un exposé de vos travaux dans le cadre de la session AFSEC de ces journées, merci de faire parvenir par email (à Olivier H Roux) un titre et un résumé de votre présentation.

Publié dans Actions Afsec, Journées | Pas de commentaire »

Journée “Robustesse dans les systèmes concurrents” le 19 octobre 2012

Tuesday 16 October 2012

4 exposés “Time constrained MSC Graph”, “la Robustesse dans les timed Petri nets”, “Une sémantique (séquentielle) alternative pour les TPN”, les “Dépendances logiques entre les événements dans les dépliages de réseaux de Petri temporels”
Discussions

Publié dans Actions Afsec, Journées | Pas de commentaire »