AFSEC

Approches Formelles des Systèmes Embarqués Communicants

journée “méthodes formelles et processus métier” le 16 octobre 2014 à Paris

Tuesday 1 July 2014

Une journée sur le thème “méthodes formelles et processus métier” (workflow, services Web, contrats QoS, …) se tiendra le 16 octobre 2014 à Paris (10h-17h15).
Organisée avec le soutien des GDR ASR et GPL.

Lieu : LIP6, Paris 6 (Jussieu) - salle 203-205 bâtiment 41 .

Le repas du midi sera offert mais une inscription (gratuite) au plus tard le 2 octobre 2014 est nécessaire
en envoyant un email à olivier-h.roux@irccyn.ec-nantes.fr ; objet : “Inscription AFSEC 16 octobre” (cliquer sur le lien) - préciser : Nom et Affiliation.

Programme :

  • 9h30-10h : Accueil (Café, viennoiseries)
  • 10h-12h30
    • Yoann LAURENT (LIP6) Alloy4SPV: a Formal Framework for Software Process Verification.
      In this work we present a framework for software process verification called Alloy4SPV which uses a subset of UML2 Activity Diagrams as a process modeling language. In order to achieve software process verification, we i) define a formal model of our process modeling language using first-order logic, ii) we give it a formal semantics based on the fUML standard, and iii) we implement this formalization using the Alloy language. In order to ease its adoption by process modelers, our framework comes with a graphical tool and a ready to use and customizable set of software process properties. We categorize these properties into two categories, syntactical and behavioral. We extend the set of behavioral properties we identified from the literature with two new categories that we defined, namely, organizational properties which relate to resource management and planning during process execution and business properties which are project/process specific properties.
    • Laurence DUCHIEN (LIFL) Une approche formelle pour la préservation de contrats de qualité de service lors de reconfiguration dynamique.
      L’omniprésence de services informatiques dans la vie quotidienne, combinée à la nature dynamique de leurs contextes d’exécution, constitue un défi majeur pour garantir la qualité attendue de ces services à l’exécution. Des contrats de Qualité de service (QoS) ont été proposés pour spécifier les niveaux de QoS attendus sur les différentes conditions de contexte, à l’aide de différents mécanismes. Dans cet exposé, nous présentons une définition des contrats de qualité de service en tant que politique de haut niveau pour régir le comportement des logiciels qui s’adaptent automatiquement à l’exécution, en réponse aux changements de contexte. Pour réaliser ce contrat, nous spécifions sa sémantique formelle et nous la mettons en œuvre dans un cadre logiciel capable d’exécuter et de reconfigurer des services, en vue de maintenir les contrats de qualité de service associés. Dans un premier temps, nous étendons les systèmes de transformation des graphes typés attribués et des machines à états finis, et nous les utilisons comme dénotations pour spécifier la sémantique des contrats de qualité de service. Deuxièmement, cette sémantique permet d’exploiter systématiquement des patrons de conception à l’exécution pour leur déploiement dynamique dans le logiciel. Troisièmement, notre sémantique garantit des propriétés d’auto-adaptation telles que la fiabilité et la robustesse dans la satisfaction de contrat. Enfin, nous évaluons l’applicabilité de notre mise en œuvre en l’intégrant et en l’exécutant dans Frascati, un middleware à base de composants multi-échelle, dans une étude de cas.
    • Nikolaos GEORGANTAS (INRIA) Service Choreographies: The Case for Interaction Paradigm Interoperability.
      With an increasing number of services and devices interacting in a decentralized manner, choreographies are an active area of investigation. The heterogeneous nature of interacting systems leads to choreographies that may not only include conventional services but also sensor-actuator networks, shared data spaces and event-based systems. Their middleware behavior within choreographies can be captured through abstract interaction paradigms, such as client-service, publish-subscribe and tuple space. This raises the essential issue of distributed system interoperability within heterogeneous choreographies. Open system integration paradigms, such as service oriented architecture (SOA) and enterprise service bus (ESB), have provided answers to the interoperability requirement. However, when it comes to integrating systems featuring heterogeneous interaction paradigms, existing solutions are typically ad hoc and partial, applying to specific interaction protocol technologies. In this talk, we introduce an interoperability solution based on abstraction and merging of the common high-level semantics of interaction paradigms, which is sufficiently general and extensible to accommodate many different protocol technologies. We apply this solution to revisit the SOA- and ESB-based integration of heterogeneous distributed systems.

  • 12h30-13h45 - Repas
  • 13h45-15h45
    • Kais KLAI (LIPN) Abstraction and Modular Verification of Inter-Enterprise Business Processes.
      Business process composition and cooperation are two important research fields in the business process domain. The questions, what properties of a process have to be public so that potential partners can collaborate with the process without risking to have an ill-designed composed process, and what is the minimal information necessary to be published, is a hot topic in the literature since many years. Also, one has to make sure that the composition of processes has the desired behaviour. The importance of dealing with such inter-enterprise business processes (IEBP for short) on one hand and business process composition on the other hand is reflected in the literature by numerous publications. In general, an IEBP can be considered as the cooperation of several local processes designed separately. The activities of each process are formally of two kinds: internal activities and cooperative activities (interface activities). IEBP are often too large for formal analysis, and the details of the components are hidden to the public so that no party knows the entire process definition. Therefore, we defend the idea that the analysis should be on the local business process and, if necessary, on an abstraction of the pertness models or of the IEBP.
      In this talk, we will present our contributions on abstraction and verification of IEBP. These contribution are mainly based on the Event-based Symbolic Observation Graph approach. Tow kinds of properties will be considered: generic properties (deadlock freeness, different variants of the soundness property) and specific properties (expressed by LTL logic).
    • Tarek MELLITI (IBISC) Formal Modelling and Evaluation of Service-based Business Process Elasticity in the Cloud.
      One of the expected features of Cloud environments is elasticity at different levels in order to guarantee provisioning of necessary resources that ensure a smooth functioning of cloud services despite changes in solicitations. Nevertheless, the provisioning of elastic infrastructures and/or platforms is not sufficient to provide users with elasticity at the level of Service-based Business Processes (SBPs). Therefore, there is a need to provide SBPs with mechanisms to scale their resource requirements up and down to ensure their adaptation to the workload changes. This can be achieved using mechanisms for duplicating and consolidating business services that compose the SBP. In this talk, we present a formal unified model (Timed Petri-nets) for SBPs elasticity. We show that our model preserves the semantics of SBPs when services are duplicated or consolidated. Based on this model, we propose a framework that defines and evaluates (by Simulation and Verification) elasticity strategies (defined as colored Petri nets). Our elasticity strategies could be a formal start to Services Level Agreement languages. The complete approach is experimented in a real Cloud environment.

  • 15h45-16h15 - Café, discussions
  • 16h15-17h
    • Pascal POIZAT (LIP6) Développement Formel de Processus Métier Chorégraphiques
      Les processus métier collaboratifs peuvent être vus selon deux perspectives complémentaires.
      Dans la première il s’agit d’inter-connecter les modèles des pairs participant à la collaboration.
      C’est une approche qui convient bien à un développement « bottom-up », par réutilisation et assemblage de pairs.
      Dans la seconde, les interactions entre pairs sont des entités de premier ordre, et il est possible de décrire les processus métiers collaboratifs d’un point de vue global, aussi appelé chorégraphique.
      Cela convient bien à un développement « top-down », par spécification et génération d’obligations locales (ou squelettes de pairs).
      Deux problèmes importants lors de la conception de processus métiers chorégraphiques (BPC) sont d’un côté la conformité entre une spécification et un ensemble de modèles de pairs
      et d’un autre côté la réalisabilité d’une spécification, c’est-à-dire la possibilité d’obtenir des modèles conformes de pairs à partir de la spécification.
      Ces problèmes ont été étudiés principalement pour des modèles interconnectés et plus récemment des modèles d’interactions.
      Par ailleurs, la prise en compte des données échangées entre les partenaires d’un processus métier collaboratif nécessite habituellement une sur-approximation ou un bornage du domaine des données.
      Dans cet exposé je présenterai des résultats récents quant à la vérification de BPC décrits dans le standard BPMN 2.0 ainsi qu’une approche symbolique basée sur l’utilisation d’un solveur SMT pour la prise en compte des données dans cette vérification.

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

Soutenance d’habilitation à diriger des recherches d’Anne Bouillard

Tuesday 24 June 2014

Anne Bouillard a présenté son mémoire habilitation à diriger des recherches intitulé “Algorithmes et efficacité du Network calculus” le 8 avril 2014. Le jury était composé de

  • M. Laurent Hardouin, Professeur
  • M. Jean-Yves Le Boudec, Professeur, rapporteur
  • M. Sylvain Lombardy, Professeur, rapporteur
  • M. Ludovic Noirie, Ingénieur de recherche
  • M. Marc Pouzet, Professeur
  • M. Jens Schmitt, Professeur, Dr.-Ing., rapporteur
  • M. Lothar Thiele, Professeur

Vous pouvez retrouver les transparents.

Publié dans WEED | Pas de commentaire »

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 »