Search

Your search keyword '"Dhaussy, Philippe"' showing total 167 results
Start Over Author "Dhaussy, Philippe"

Refine your results

more »

more »

more »

more »
167 results on '"Dhaussy, Philippe"'

2. A Problem-Oriented Approach to Critical System Design and Diagnosis Support

Author

Leildé, Vincent, Ribaud, Vincent, Teodorov, Ciprian, Dhaussy, Philippe, Barbosa, Simone Diniz Junqueira, Series Editor, Filipe, Joaquim, Series Editor, Kotenko, Igor, Series Editor, Sivalingam, Krishna M., Series Editor, Washio, Takashi, Series Editor, Yuan, Junsong, Series Editor, Zhou, Lizhu, Series Editor, Ghosh, Ashish, Series Editor, Abdelwahed, El Hassan, editor, Bellatreche, Ladjel, editor, Benslimane, Djamal, editor, Golfarelli, Matteo, editor, Jean, Stéphane, editor, Mery, Dominique, editor, Nakamatsu, Kazumi, editor, and Ordonez, Carlos, editor

Published
2018
Full Text
View/download PDF

3. Using Parallel and Distributed Reachability in Model Checking

Author

Allal, Lamia, Belalem, Ghalem, Dhaussy, Philippe, Teodorov, Ciprian, Kacprzyk, Janusz, Series Editor, Pal, Nikhil R., Advisory Editor, Bello Perez, Rafael, Advisory Editor, Corchado, Emilio S., Advisory Editor, Hagras, Hani, Advisory Editor, Kóczy, László T., Advisory Editor, Kreinovich, Vladik, Advisory Editor, Lin, Chin-Teng, Advisory Editor, Lu, Jie, Advisory Editor, Melin, Patricia, Advisory Editor, Nedjah, Nadia, Advisory Editor, Nguyen, Ngoc Thanh, Advisory Editor, Wang, Jun, Advisory Editor, Perez, Gregorio Martinez, editor, Tiwari, Shailesh, editor, Trivedi, Munesh C., editor, and Mishra, Krishn K., editor

Published
2018
Full Text
View/download PDF

4. Embedded UML Model Execution to Bridge the Gap Between Design and Runtime

Author

Besnard, Valentin, Brun, Matthias, Jouault, Frédéric, Teodorov, Ciprian, Dhaussy, Philippe, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Mazzara, Manuel, editor, Ober, Iulian, editor, and Salaün, Gwen, editor

Published
2018
Full Text
View/download PDF

5. Domain-Oriented Verification Management

Author

Leildé, Vincent, Ribaud, Vincent, Teodorov, Ciprian, Dhaussy, Philippe, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Abdelwahed, El Hassan, editor, Bellatreche, Ladjel, editor, Golfarelli, Mattéo, editor, Méry, Dominique, editor, and Ordonez, Carlos, editor

Published
2018
Full Text
View/download PDF

6. A Diagnosis Framework for Critical Systems Verification (Short Paper)

Author

Leildé, Vincent, Ribaud, Vincent, Teodorov, Ciprian, Dhaussy, Philippe, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Cimatti, Alessandro, editor, and Sirjani, Marjan, editor

Published
2017
Full Text
View/download PDF

7. Proposed Algorithms to the State Explosion Problem

Author

Allal, Lamia, Belalem, Ghalem, Dhaussy, Philippe, Teodorov, Ciprian, Filipe, Joaquim, Editorial Board Member, Ghosh, Ashish, Editorial Board Member, Kotenko, Igor, Editorial Board Member, Prates, Raquel Oliveira, Editorial Board Member, Zhou, Lizhu, Editorial Board Member, Barbosa, Simone Diniz Junqueira, Editorial Board Member, Chen, Phoebe, Editorial Board Member, Du, Xiaoyong, Editorial Board Member, Kara, Orhun, Editorial Board Member, Liu, Ting, Editorial Board Member, Sivalingam, Krishna M., Editorial Board Member, Washio, Takashi, Editorial Board Member, Yuan, Junsong, Editorial Board Member, Unal, Aynur, editor, Nayak, Malaya, editor, Mishra, Durgesh Kumar, editor, Singh, Dharm, editor, and Joshi, Amit, editor

Published
2016
Full Text
View/download PDF

9. An Organizing System to Perform and Enable Verification and Diagnosis Activities

Author

Leilde, Vincent, Ribaud, Vincent, Dhaussy, Philippe, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Yin, Hujun, editor, Gao, Yang, editor, Li, Bin, editor, Zhang, Daoqiang, editor, Yang, Ming, editor, Li, Yun, editor, Klawonn, Frank, editor, and Tallón-Ballesteros, Antonio J., editor

Published
2016
Full Text
View/download PDF

11. Sequential and Parallel Algorithms for the State Space Exploration

Author

Allal Lamia, Belalem Ghalem, Dhaussy Philippe, and Teodorov Ciprian

Subjects
model checking, state explosion problem, sequential exploration, parallel exploration, Cybernetics, Q300-390
Abstract

In this article, we are interested in the exploration part of model checking which consists in traversing all the possible states of a system. We propose two approaches to exploration, parallel and sequential. We present a comparison between our parallel approach and the parallel algorithm proposed in SPIN.

Published
2016
Full Text
View/download PDF

13. Context-Aware Verification of a Landing Gear System

Author

Dhaussy, Philippe, Teodorov, Ciprian, Junqueira Barbosa, Simone Diniz, editor, Chen, Phoebe, editor, Cuzzocrea, Alfredo, editor, Du, Xiaoyong, editor, Filipe, Joaquim, editor, Kara, Orhun, editor, Kotenko, Igor, editor, Sivalingam, Krishna M., editor, Ślęzak, Dominik, editor, Washio, Takashi, editor, Yang, Xiaokang, editor, Boniol, Frédéric, editor, Wiels, Virginie, editor, Ait Ameur, Yamine, editor, and Schewe, Klaus-Dieter, editor

Published
2014
Full Text
View/download PDF

14. Context-Aware Verification of a Cruise-Control System

Author

Teodorov, Ciprian, Leroux, Luka, Dhaussy, Philippe, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Ait Ameur, Yamine, editor, Bellatreche, Ladjel, editor, and Papadopoulos, George A., editor

Published
2014
Full Text
View/download PDF

16. A Transformation Approach for Multiform Time Requirements

Author

Menad, Nadia, Dhaussy, Philippe, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Hierons, Robert M., editor, Merayo, Mercedes G., editor, and Bravetti, Mario, editor

Published
2013
Full Text
View/download PDF

17. Use Cases for Context Aware Model-Checking

Author

Raji, Amine, Dhaussy, Philippe, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Kienzle, Jörg, editor

Published
2012
Full Text
View/download PDF

18. Context-aware approach for formal verification

Author

Amel Benabbou, Safia Nait Bahloul, and Dhaussy Philippe

Subjects
Context, Context-awareness, Context-aware verification, Model-checking, Model transformation, Use cases, Interaction overview diagram, Technology (General), T1-995
Abstract

The Context-aware approach has proven to be an effective technique for software model-checking verification. It focuses on the explicit modelling of environment as one or more contexts. In this area, specifying precise requirement is a challenged task for engineer since often environmental conditions lack of precision. A DSL, called CDL, has been proposed to facilitate the specification of requirement and context. However, such language is still low-level and error prone, difficult to grasp on complex models and assessment about its usability is still mitigated. In this paper, we propose a high level formalism of CDL to facilitate specifying contexts based on interaction overview diagrams that orchestrate activity diagrams automatically transformed from textual use cases. Our approach highlights the boundaries between the system and its environment. It is qualified as model checking context-aware that aims to reduce the semantic gap between informal and formal requirements, hence the objective is to assist and encourage engineers to put sufficient details to accomplish effectively the specification process.

Published
2016
Full Text
View/download PDF

19. Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation

Author

Dhaussy, Philippe, Pillain, Pierre-Yves, Creff, Stephen, Raji, Amine, Le Traon, Yves, Baudry, Benoit, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Schürr, Andy, editor, and Selic, Bran, editor

Published
2009
Full Text
View/download PDF

24. SDL as UML: Why and What Panel

Author

Selic, Bran, Dhaussy, Philippe, Ek, Anders, Haugen, Øystein, Leblanc, Philippe, Møller-Pedersen, Birger, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, France, Robert, editor, and Rumpe, Bernhard, editor

Published
1999
Full Text
View/download PDF

31. Data Management Mechanisms for Internet of Things: A Position Paper

Author

Diallo Ousmane, Teodorov Ciprian, Dhaussy Philippe, University of Assane Seck, Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT), The American Council on Science and Education, and IEEE Computer Society

Subjects
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR], [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Distributed database, IoT data types, Smart objects, Computer science, business.industry, Data management, Internet of Things, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], 020208 electrical & electronic engineering, 05 social sciences, 050301 education, 02 engineering and technology, Data science, Analytics, Computer data storage, 0202 electrical engineering, electronic engineering, information engineering, Position paper, The Internet, Key challenges, business, 0503 education
Abstract

International audience; Internet of Things (IoT) is a network where several and various interconnected, smart objects continuously generate alarge amount of data transmitted over Internet. Several efforts and research works in IoT focused on hardware constraints, lowcost, application design, as well as good communication technologies. However, due to the intrinsic characteristics of diversity,heterogeneity, large-scale, dynamic and large volume of data generated and various IoT applications needs, using traditionaldatabase management mechanisms and analytics architectures is not generally suitable. Then, it is challenging to provideefficient IoT data storage and query processing mechanisms for satisfying IoT application needs. This paper identifies the mainspecifications and mechanisms of data and query management for IoT and classifies them. Moreover, this work presentsadvances on data and query management mechanisms on IoT, shows their advantages and limits and discusses the challengingopen research issues that need to be addressed for providing guidelines for further contributions.

Published
2019
Full Text
View/download PDF

32. EMI : Un Interpréteur de Modèles Embarqué pour l’Exécution et la Vérification de Modèles UML

Author

Besnard, Valentin, Brun, Matthias, Dhaussy, Philippe, Jouault, Frédéric, Teodorov, Ciprian, ESEO-ÉRIS (ÉRIS), ESEO-Tech, Université Bretagne Loire (UBL)-Université Bretagne Loire (UBL), Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)

Subjects
Interprétation de modèles, Model-checking, [INFO]Computer Science [cs], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Systèmes embarqués, UML
Abstract

National audience; Pour faire face à la complexité croissante des systèmes embarqués, les activités de vérification et de validation, et notamment le model-checking,sont de plus en plus sollicités. Les model-checkers permettent de vérifier des propriétés par rapport au modèle formel fourni en entrée mais deux problèmes subsistent généralement. D’une part, les outils de model-checking n’apportent pas l’assurance que les propriétés sont aussi vérifiées sur le code exécutable du système. D’autre part, le modèle formel utilisé par les modelcheckers est souvent le résultat d’une transformation de modèle dont l’exactitude n’est pas prouvée. Pour y remédier, cet article présente EMI, un interpréteur de modèles UML visant l’exécution et la vérification de systèmes embarqués à l’aide d’une seule implémentation de la sémantique du langage. En connectant cet outil au model-checker OBP2, diverses activités de vérification peuvent ainsi être menées sur des modèles semi-formels en UML.

Published
2019

34. Model-checking for Secured Component Implementation

Author

Fadi, Obeid, Dhaussy, Philippe, Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)

Subjects
[INFO]Computer Science [cs], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Abstract

International audience; A security pattern is a reusable solution for a specific security issue. Based on an insecure model, and using a combination of security patterns, we can generate a model respecting some security requirements constituting a security policy. The resulting model needs to fulfill the security requirements without affecting the original functionalities and services. The security patterns need to be consistent with eachothers, as well as the model, they also need to cover the whole security spectrum resulting in completeness. We can use model checking techniques in order to insure the correct functionality, as well as the consistency and completeness of the generated model. In this paper, we describe our approach to combine an architectural model with security patterns to generate a secure model. This model is later verified using model checking techniques to validate the properties of the model itself as well as the used patterns. Finally, using an experimental use case, we demonstrate the possible spatial complexity of our approach.

Published
2018

35. Secure Communication Protocol: Application to Large Number of Distributed Sensors

Author

Fadi, Obeid, Dhaussy, Philippe, Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)

Subjects
ComputerApplications_COMPUTERSINOTHERSYSTEMS, [INFO]Computer Science [cs], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Abstract

International audience; Supervisory control and data acquisition (SCADA) systems control many of our critical industrial infrastructures. Currently, most SCADA systems are considered insecure due to their lack of security measures. The increased number of connections between SCADA systems along with other factors, caused an augmentation in the threats and attacks on SCADA. Many solutions were proposed to secure SCADAcommunications. However, any undertaken security measure while communicating unencrypted messages would not be robustin case of attacks. The numerous embedded devices used in SCADA make it hard to consider classic cryptography, although,some SCADA systems already implemented such algorithms.In this paper, we present a new approach to secure SCADA communications by using dynamically modified signals instead of plain or encrypted messages. Our solution can be implemented in low cost electrical chips (used on sensors, switches, etc.) or as a software (used on servers, etc.). The Reconfigurable Information Transmitter Agent (RITA) protocol that we present can also be used to secure any type of communication that respects the protocol’s constraints. The solution, while still lacking the necessary analysis to ensure its security level, ispromising. This approach is planned to be implemented on a large number of distributed underwater sensors.

Published
2018

36. Validation formelle d’architecture logicielle basée sur des patrons de sécurité

Author

Fadi, Obeid, Dhaussy, Philippe, Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT), Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)

Subjects
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO]Computer Science [cs], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Abstract

National audience; Les modèles de patrons de sécurité ont été proposés comme des solutions méthodologiques permettant de modéliser des mécanismes qui répondent à des problèmes de sécurité récurrents. Ceux-ci sont décrits dans la littérature et peuvent être exploités dans différents contextes de modélisation. Lors de leur intégration au sein d’un modèle d’architecture, ces modèles de patrons sont à adapter à ses spécificités. Une fois les modèles de patrons intégrés, il est nécessaire de valider formellement le résultat de cette intégration au regard des propriétés fonctionnelles de l’architecture initiale qui doivent être préservées, et au regard des propriétés formelles de sécurité associées aux patrons.Dans notre travail, nous exploitons une technique de model-checking pour la vérification des propriétés. Nous cherchons à exploiter notre approche dans le cadre de la modélisation des architectures SCADA.

Published
2018

39. Technological choices for dense networks of small sensors

Author

Rolin, Jean-francois, Loubrieu, Thomas, Delauney, Laurent, Carotenuto, Federico, Dhaussy, Philippe, Obeid, Fadi, Delory, Eric, Rolin, Jean-francois, Loubrieu, Thomas, Delauney, Laurent, Carotenuto, Federico, Dhaussy, Philippe, Obeid, Fadi, and Delory, Eric

Abstract

Small, generally low-cost sensors, that are deployed in unsupervised networks (or remote locations such as the ocean) are becoming more and more important across RIs and across domain. Distributed infrastructures require efficient data transmission through a more strict effort on standards for sensor registration, sensor web enablement, sensor-embedded treatment capacities. Network-enabled sensors offer a strong potential. This deliverable will present ongoing initiatives and proves the maturity and security of the smart sensor techniques applied at large scale.

Published
2019

40. Towards one Model Interpreter for Both Design and Deployment

Author

Besnard, Valentin, Brun, Matthias, Dhaussy, Philippe, Jouault, Frédéric, Olivier, David, Teodorov, Ciprian, ESEO-TRAME (TRAME), ESEO-Tech, Université Bretagne Loire (UBL)-Université Bretagne Loire (UBL), Pôle STIC_IDM, École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne), Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL), Davidson Consulting, École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)

Subjects
Embedded Systems, Model Verification, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Model Interpretation, UML
Abstract

International audience; Executable modeling of complex embedded systems is essential for bug discovery and safety validation at early designstages. A relatively large number of tools enable early design diagnosis and validation by transforming and analyzing themodel into a formal setting. However, this transformation induces a semantic gap rendering diagnosis more difficult. Moreover, on the way to deployment, executable models are transformed into low level executable code. Existence of this second transformation similarly renders diagnosis of the deployed system more difficult,and also increases validation costs of the approach in the context of critical systems: a non trivial equivalence relation needs to be established between the formally analyzed model and the executable code. In this paper, we introduce a first step towards addressing these problems with a bare-metal UML interpreter, which uniquely defines the executable semantics for both design and deployment. To facilitate the diagnosis and validation processour interpreter offers a diagnosis interface through which the semantics is shared with diagnosis tools. The tools rely on this interface to interact with (observe and control) the executing model either locally on a PC during early design phases or remotely on the target embedded system after deployment. We illustrate our approach on a railway level crossing system ported to two embedded targets (at91sam7s and stm32), to which weconnect a remote high-level simulator for interactive execution control and exhaustive state-space exploration.

Published
2017

41. A Diagnosis Framework for Critical Systems Verification

Author

Leilde, Vincent, Ribaud, Vincent, Teodorov, Ciprian, Dhaussy, Philippe, 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), Lab-STICC_UBO_CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-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)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-École Nationale d'Ingénieurs de Brest (ENIB)-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)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Ribaud, Vincent, 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 Brest (UBO)-Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), and Université de Brest (UBO)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM)

Subjects
[INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], Diagnosis, Framework, Verification, ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.5: Testing and Debugging/D.2.5.2: Diagnostics, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Critical systems, ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking
Abstract

International audience; For critical systems design, the verification tasks play a crucial role. If abnormalities are detected, a diagnostic process must be started to find and understand the root causes before corrective actions are applied. Detection and diagnosis are notions that overlap in common speech. Detection basically means to identify something as unusual, diagnosis means to investigate its root cause. The meaning of diagnosis is also fuzzy, because diagnosis is either an activity-an investigation-or an output result-the nature or the type of a problem. This paper proposes an organizational framework for structuring diagnoses around three principles: that propositional data (including detection) are the inputs of the diagnostic system; that activities are made of methods and techniques; and that associations specialize that relationships between the two preceding categories.

Published
2017

44. Past-Free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis

Author

Teodorov, Ciprian, Roux, Luka Le, Drey, Zoé, Dhaussy, Philippe, Lab-STICC_ENSTAB_ CACS_MOCS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT), Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-Institut Mines-Télécom [Paris] (IMT)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)

Subjects
reachability analysis, [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], context-aware verification, formal verification, directed-acyclic graph, semi-external algorithms
Abstract

International audience; Model-checking enables the automated formal verification of software systems through the explicit enumeration of all the reachable states. While this technique has been successfully applied to industrial systems, it suffers from the state-space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. In this paper, we present a new reachability analysis algorithm, named Past-Free[ze], that reduces the state-space explosion problem by freeing parts of the state-space from memory. This algorithm relies on the explicit isolation of the acyclic parts of the system before analysis. The parallel composition of these parts drives the reachability analysis, the core of all model-checkers. During the execution, the past states of the system are freed from memory making room for more future states. To enable counter-example construction, the past states can be stored on external storage. To show the effectiveness of the approach, the algorithm was implemented in the OBP Observation Engine and was evaluated both on a synthetic benchmark and on realistic case studies from automotive and aerospace domains. The benchmark, composed of 50 test cases, shows that in average, 75% of the state-space can be dropped from memory thus enabling the exploration of up to 14 times more states than traditional approaches. Moreover, in some cases, the reachability analysis time can be reduced by up to 25%. In realistic settings, the use of Past-Free[ze] enabled the exploration of a state-space 4.5 times larger on the automotive case study, where almost 50% of the states are freed from memory. Moreover, this approach offers the possibility of analyzing an arbitrary number of interactions between the environment and the system-under-verification; for instance, in the case of the aerospace example, 1000 pilot/system interactions could be analyzed unraveling an 80 GB state-space using only 10 GB of memory

Published
2016
Full Text
View/download PDF

45. Towards a Transformation Approach of Timed UML MARTE Specifications for Observer-Based Formal Verification

Author

Menad, Nadia, Dhaussy, Philippe, Drey, Zoé, Mekki, Rachida, Lab-STICC_ENSTAB_CACS_COM, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-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)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-École Nationale d'Ingénieurs de Brest (ENIB)-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)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Pôle STIC_IDM, École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne), Université des sciences et de la Technologie d'Oran Mohamed Boudiaf [Oran] (USTO MB), and Billon-Coat, Annick

Subjects
[INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Formal verification, observer automata, [INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC], [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], Formal verification, model-checking, CCSL time constraints, observer automata, CCSL time constraints, Software Engineering, [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], model-checking, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Abstract

International audience; Modeling timing constraints of distributed systems and multi-clock elec-tronic systems aims to describe different time requirements aspects at a higher ab-straction level. An important aspect is the logical time of the behavior of thesesystems. To model the time requirements, a specification language with multipleclock domains called Clock Constraint Specifiation Language (CCSL) has been in-troduced, in order to enrich the formalisms of existing modeling tools and also tofacilitate the description and analysis of temporal constraints. Once the softwarehas been modeled, the difficulty lies in both expressing the relevant properties andverifying them formally. For that purpose formal transformation techniques mustbe introduced. However, it remains difficult to exploit initial models as such, and tointegrate them into a formal verification process. This paper introduces a method-ology and the original tool chain for exploiting UML MARTE models enriched withCCSL specification. These will be integrated together with a range of tools forexpressing and verifying time constraints. We propose a more general translationapproach that verifies not only CCSL constraints implementations but also prop-erties of the complete model including all the functional components. We evaluateour approach with a case study.

Published
2016

49. Context-aware approach for formal verification

Author

Safia Nait Bahloul, Dhaussy Philippe, Amel Benabbou, 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), University of Oran Es-Senia [Oran] | Université d'Oran Es-Senia [Oran], IDM, Pôle STIC [Brest] (STIC), École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-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)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-École Nationale d'Ingénieurs de Brest (ENIB)-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)-Université européenne de Bretagne - European University of Brittany (UEB)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), and University of Oran Es-Sénia [Oran]

Subjects
Context-awareness, Computer science, Model transformation, Use cases, Context (language use), Activity diagram, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], lcsh:Technology (General), Use case, Formal verification, computer.programming_language, business.industry, Interaction overview diagram, Context, Usability, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Model-checking, Context-aware verification, Systems engineering, lcsh:T1-995, Software engineering, business, computer, Semantic gap
Abstract

International audience; The Context-aware approach has proven to be an effective technique for software model-checking verification. It focuseson the explicit modelling of environment as one or more contexts. In this area, specifying precise requirement is achallenged task for engineer since often environmental conditions lack of precision. A DSL, called CDL, has beenproposed to facilitate the specification of requirement and context. However, such language is still low-level and errorprone, difficult to grasp on complex models and assessment about its usability is still mitigated. In this paper, we propose ahigh level formalism of CDL to facilitate specifying contexts based on interaction overview diagrams that orchestrateactivity diagrams automatically transformed from textual use cases. Our approach highlights the boundaries between thesystem and its environment. It is qualified as model-checking context-aware that aims to reduce the semantic gap betweeninformal and formal requirements, hence the objective is to assist and encourage engineers to put sufficient details toaccomplish effectively the specification process.

Published
2016
Full Text
View/download PDF

50. Model Checking of SCADE Designed Systems

Author

Heim, S, Dumas, Xavier, Bonnafous, E, Dhaussy, Philippe, Teodorov, C, Leroux, Lise, Boyer, Marc, Communication & Systèmes [Toulouse] (C-S), Communication & Systèmes-CS-SI France, 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), Pôle STIC_IDM, École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne), 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), and Université de Brest (UBO)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)

Subjects
OBP, asynchronous, formal methods, synchronous, CDL, SCADE, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, LUSTRE, model checking, [INFO.INFO-ES] Computer Science [cs]/Embedded Systems
Abstract

International audience; Model checking is a well-known method to verify a formal model in all possible configurations. Nevertheless this technique can hardly scale up to industrial asynchronous systems because of the state-space explosion problem. To address this challenge, a new approach based on context specification (the environment of the system) and an observation engine called OBP (Observer Based Prover) has been developed. The idea is that given a property to be verified, one doesn’t need to explore all possible configurations of the complete system. Among all possible behavior of the system, a tiny part is representative enough for the property to be verified. Thus, specifying a pertinent environment (a context) allows restricting the system behavior on those only parts where the property is worth verifying.The objective of our work is to apply this Context-aware verification method to the verification of SCADE systems designed in LUSTRE language, in order to check behavioral properties related to system safety. Moreover LUSTRE is a synchronous language whereas OBP exploration engine takes as input an asynchronous model designed in FIACRE language. To cope with this problem our approach consists in developing a GALS method combining asynchronous contexts with synchronous models.

Published
2016

Catalog

Books, media, physical & digital resources
See catalog results