logo EDITE Yann BEN MAISSA
Identité
Yann BEN MAISSA
État académique
Thèse soutenue le 2013-09-21
Sujet: Modélisation et vérification de Modélisation et vérification de systèmes embarqués critiques : application à des réseaux de capteurs sans fil
Direction de thèse:
Laboratoire:
Voisinage
Ellipse bleue: doctorant, ellipse jaune: docteur, rectangle vert: permanent, rectangle jaune: HDR. Trait vert: encadrant de thèse, trait bleu: directeur de thèse, pointillé: jury d'évaluation à mi-parcours ou jury de thèse.
Productions scientifiques
oai:hal.archives-ouvertes.fr:hal-00822408
Modeling and Analyzing Wireless Sensor Networks with VeriSensor
A Wireless Sensor Network (WSN), made of distributed autonomous nodes, is designed to monitor physical or environmental conditions. WSNs have many application domains such as environment or health monitoring. Their de- sign must consider energy constraints, concurrency issues, node heterogeneity, while still meeting the quality requirements of life-critical applications. Formal verification helps to obtain WSN reliability, but usually requires a high expertise, which limits its adoption in industry. This paper presents VeriSensor, a domain specific modeling language (DSML) for WSNs offering support for formal verification. VeriSensor is designed to be used by WSN experts. It can be automatically translated into a formal specifica- tion for model checking. We present the language, its translation, show how they work on a simple case study, and illustrate how several metrics and properties relevant to the domain can be evaluated.
Petri Net and Software Engineering (PNSE) Petri Nets for Software Engineeringconference proceeding 2012
oai:hal.archives-ouvertes.fr:hal-00822416
Hierarchy is Good For Discrete Time: a Compositional Approach to Discrete Time Verification
Model checking is now widely used as an automatic and exhaustive way to verify complex systems. However, this approach suffers from an intrinsic combinatorial explosion, due to both a high number of synchronized components and a high level of expressivity in these components. With respect to the expressivity issue, we consider the particular problem of introducing explicit time constraints in the components of a system. In this modeling step, the choice of a time domain is important, impacting on the size of the resulting model, the class of properties which can be verified and the performances of the verification. In this presentation, we show that hierarchical encoding of elementary com- ponents encapsulating labeled transition systems (LTS), synchronized by means of public transitions, is an efficient way to encode discrete time.
Dagstuhl seminar "Architecture-Driven Semantic Analysis of Embedded Systems" Dagstuhl seminarconference proceeding 2012-07
oai:hal.archives-ouvertes.fr:hal-00840207
Un langage de modélisation pour réseaux de capteurs sans fil basé sur sysml
2èmes Journées Doctorales en Technologies de l'Information et de la Communicationconference, seminar, workshop communication 2010-07-15
oai:hal.archives-ouvertes.fr:hal-00840206
A SysML profile for wireless sensor networks modeling
Today, wireless sensor networks designers do not fully benefit from the power of widely recognized UML (and its profiles including SysML) when it comes to modeling all aspects of a wireless sensor network. The modeling process is usually restricted to the software and therefore only partially supports the wireless sensor network's design. Among the UML profiles family, there is a language that supports the modeling of many aspects of a system (including software and hardware) : SysML (Systems Modeling Language). In this paper, we propose a SysML profile for wireless sensor networks that will support the modelling of such networks. This profile provides support for structure, behavior, requirements and energy consumption information modeling. It will allow designers to model different aspects of a wireless sensor network.
I/V Communications and Mobile Network (ISVC), 2010 5th International Symposium on I/V Communications and Mobile Network (ISVC), 2010 5th International Symposium onconference proceeding 2010-09-30
oai:hal.archives-ouvertes.fr:hal-00840204
Modeling and Analyzing Wireless Sensor Networks with VeriSensor: an Integrated Workflow
A Wireless Sensor Network (WSN), made of distributed autonomous nodes, is designed to monitor physical or environmental conditions. WSN have many application domains such as environment or health monitoring. Their de- sign must consider energy constraints, concurrency issues, node heterogeneity, while still meeting the quality requirements of life-critical applications. Formal verification helps to obtain WSN reliability, but usually requires a high expertise, which limits its adoption in industry. This paper presents VeriSensor, a domain specific modeling language (DSML) for WSN offering support for formal verification. VeriSensor is designed to be used by WSN experts. It can be automatically translated into a formal specifica- tion for model checking. We present the language and its translation into a formal model (we use Instantiable Transition Systems - ITS). A tool has been implemented. We used it to work on a case study, illustrating how several metrics and properties relevant to the domain can be evaluated.
Transactions on Petri Nets and Other Models of Concurrencyarticle in peer-reviewed journal 2013-07-31
Soutenance
Thèse: Contribution à la modélisation et à la vérification de réseaux de capteurs sans fil.
Soutenance: 2013-09-21
Rapporteurs: Youssef FAKHRI    Laure PETRUCCI