=Paper=
{{Paper
|id=Vol-1689/preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1689/preface.pdf
|volume=Vol-1689
}}
==None==
https://ceur-ws.org/Vol-1689/preface.pdf
Mohamed G HAZEL, IFSTTAR, Lille, France
Mohamed J MAIEL, DRC & ReDCAD, ENIS-University of Sfax, Sfax, Tunisia
VECoS’2016
Verification and Evaluation of Computer and Communication
Systems
10th International Workshop
Tunis, Tunisia, October 6-7, 2016
Proceedings
c Copyright 2016 for the individual papers by the papers’ authors. Copying permitted for private and academic purposes. This volume is published and copyrighted
by its editors.
These proceedings are published online by the editors as Volume 1689 at
CEUR Workshop Proceedings
ISSN 1613-0073
http://ceur-ws.org/Vol-1689
PREFACE
These are the proceedings of the 10th International Workshop on Verification and Evaluation of Computer and
Communication Systems (VECoS’2016) held the 6th and 7th of October 2016 at the Tunisia Polytechnic School
that is the main organizer together with the support of Digital Research Center of Sfax, MeFoSyLoMa Group and
Formal Methods Europe.
The International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS)
was created by an Euro-Mediterranean network of researchers in computer science. Its first edition, VECoS 2007,
took place in Algiers, VECoS 2008 in Leeds, VECoS 2009 in Rabat, VECoS 2010 in Paris, and VECoS 2011 in Tunis,
VECoS 2012 in Paris, VECoS 2013 in Florence, VECoS 2014 in Bejaia and VECos 2015 in Bucharest.
The aim of the VECoS workshop is to bring together researchers and practitioners, in the areas of verification,
control, performance, quality of service, dependability evaluation and assessment, in order to discuss the state-
of-the-art,the new developments and the challenges in modern computer and communication systems in which
functional and extra-functional properties are strongly interrelated. Thus, the main motivation for VECoS is to
encourage the cross-fertilization between the various formal verification and evaluation approaches, methods
and techniques, especially those developed for concurrent and distributed hardware/software systems.
Beyond its technical and scientific goals, another main purpose of VECoS is to promote collaboration
between participants in research and education in the area of computer science and engineering. We welcome
contributions describing original research, practical experience reports and tool descriptions/demonstrations in
the areas of verification, control, performance, quality of service and dependability evaluation.
The invited speakers for VECoS 2015 are: Eric Badouel from SUMO, IRISA Rennes and Serge Haddad from LSV,
ENS Cachan, France.
We received 26 contributions which have been thoroughly reviewed for originality, significance and relevance
(108 reviews in total). For each paper three to five reviews were made. The program committee has accepted 13
papers for full presentation.
Without support of our academic and corporate sponsors, the enormous effort of authors, reviewers, steering
committee and the local organizational team this tenth workshop wouldn’t provide such an interesting program.
We would like to thank all these persons.
We also thank the authors for their submissions and the program committee members for their hard work.
October 2016 Mohamed G HAZEL and Mohamed J MAIEL
3
ORGANIZING COMMITTEE
Abichou Azgal, Tunisia Polytechnic School (General Emna Kalai, Tunisia Polytechnic School
Chair) Hela Ben Salah, Tunisia Polytechnic School
Adel Benzina, Tunisia Polytechnic School (Chair) Aymen Gammoudi, Tunisia Polytechnic School
Takoua Abdellatif, Tunisia Polytechnic School
STEERING COMMITTEE
Hassane Alla, GIPSA Lab, INPG Grenoble Mohamed Kaaniche, LAAS CNRS, Toulouse
Djamil Aissani, LAMOS, Université de Bejaia Bruno Monsuez, ENSTA - UIIS, Paris
Kamel Barkaoui, CEDRIC, CNAM Paris (Chair) Nihal Pekergin, LACL UPEC, Créteil
Hanifa Boucheneb, Ecole Polytechnique de Montréal Denis Poitrenaud, LIP6 UPMC, Paris
Francesco Flammini, Ansaldo STS, Milano Tayssir Touili, LIAFA, Université Paris Diderot
PROGRAM COMMITTEE
Takoua Abdellatif, EPT, Tunis Chadlia Jerad, ENSI, Tunis
Djamil Aissani, LAMOS, Bejaia Mohamed Jmaiel, DRC & ReDCAD, Sfax , Tunisia (co-
Hassane Alla, GIPSA, Grenoble chair)
Yamine Ait Ameur, IRIT/ENSEEIHT, Toulouse Jorge Julvez, University of Zaragoza
Mohamed Faouzi Atig, Uppsala University Mohamed Kaaniche, LAAS, Toulouse
Kamel Barkaoui, Cedric Cnam, Paris Kais Klai, LIPN , Villetaneuse
Faı̈za Belala, LIRE, IC2, Algeria Ouajdi Korbaa, LI3, ISITCom, Sousse
Saddek Bensalem, VERIMAG Grenoble, France Moez Krichen, Albaha University, KSA
Adel Benzina, LESCN-EPT, Tunis Lars Michael Kristensen, Bergen University College,
Mohamed Tahar Bhiri, ISIM, Sfax Bergen
Simon Bliudze, EPFL, Lausanne Zhiwu Li, Xidian Univ, Xian
Patrice Bonhomme, LI, University of Tours Gaiyun Liu, Xidian Univ., Xian
Frédéric Boniol, ONERA, Toulouse Mourad Maouche, Philadephia University, Amman
Abdelmadjid Bouabdallah, Heudiasyc Lab, Compiegne Louiza Bouallouche Medjkoune, LAMOS, Bejaia
Ahmed Bouajjani, LIAFA, Paris Otmane Ait Mohamed, Concordia University, Montreal
Hanifa Boucheneb, Ecole Polytechnique de Montréal Bruno Monsuez, ENSTA ParisTech, Saclay
Mahmoud Boufaida, LIRE Univ. Constantine 2 Mohamed Mosbah, LaBRI, Bordeaux
Florian Brandner, Telecom ParisTech Hassan Mountassir, LIFC University Franche-Comté
Awatef Hicheur Cairns, Cedric, Cnam, Paris Ayoub Nouri, Cea Leti, Grenoble
Annie Choquet-Geniet, LISI, Ensma, Poitiers Meriem Ouederni, IRIT, Toulouse
Feng Chu, IBISC, Evry Mourad Oussalah, LINA, Nantes
Gabriel Ciobanu, Romanian Academy, ICS, Iasi Claire Pagetti, ONERA, Toulouse
Liliana Cucu-Grosjean, INRIA Paris-Rocquencourt Vladimir-Alexandru Paun, ENSTA ParisTech, Saclay
Isabel Demongodin, LSIS Marseille Nihal Pekergin, LACL, Créteil
Josée Desharnais, Université Laval, Quebec Olivier Perrin, INRIA-LORIA, Nancy
Karim Djouani, LISSI UPEC, Créteil Denis Poitrenaud, LIP6, Paris
Lamia Atma Djoudi, Synchrone Technologies, Paris Narjess Ben Rejeb, INSAT, Tunis
Mohammed Erradi, ENSIAS, Rabat Ahmed Rezine, Linköping University
Mohamed Escheikh, ENIT,Tunis Riadh Robbana, INSAT, Tunis
Alessandro Fantecchi, Unifi, Italy Zaı̈di Sahnoun, LIRE, Constantine
Francesco Flammini, Ansaldo STS, Milano Zohra Sbaı̈, ENIT, Tunis
Fabio Gadducci, CSD, University of Pisa Carla Seatzu, University of Cagliari
Mohamed Ghazel, IFSTTAR, Lille (co-chair) Larbi Sekhri, Univ. es Senia, Oran
Khaled Ghedira, ANPR, Tunis Ahmed Serhrouchni, Telecom ParisTech
Latéfa Ghomri, University of Tlemcen Sofiene Tahar, Concordia University
Mohamed Graiet, MIRACL, Monastir Nicolae Tapus, University POLITEHNICA of Bucharest
Mohand-Said Hacid , LIRIS, Lyon Nadia Tawbi, Université Laval, Quebec
Serge Haddad, LSV ENS Cachan Thouraya Tebibel, ESI, Alger
Ahmed Hadj-Kacem, ReDCAD, Sfax Tayssir Touili, LIPN Villetaneuse
Imen Ben Hafaiedh, LIP2 ISI , Tunis Farouk Toumani, LIMOS, Clermont-Ferrand
Belgacem Ben Hedia, LIST-CEA, Saclay Ahlem Triki, VERIMAG Grenoble
Bernd Heidergott, VU Amsterdam University Florin Popentiu Vladicescu, University of Oradea
Malika Ioulalen, USTHB Alger Karsten Wolf, Universitaet Rostock
Mohamad Jaber, American University of Beirut Habib Youssef, ISITCom Sousse
Ali Jaoua, C.E, Qatar University Belhassen Zouari, SupCom
4
CONTENTS
I Session: Probabilistic verification 7
Exact and Approximate Diagnosis of Probabilistic Systems (Invited talk)
Serge H ADDAD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Performance Evaluation of Complex Systems Using the SBIP Framework
Ayoub N OURI, Marius B OZGA, Axel L EGAY and Saddek B ENSALEM . . . . . . . . . . . . . . . . . . . 11
Statistical Model Checking of CSMA/CA in WSNs
Zohra H MIDI, Laid K AHLOUL, Saber B ENHARZALLAH and Cherifa O THMANE . . . . . . . . . . . . . 27
Formal Probabilistic Analysis of Lifetime for a WSN-based Monitoring Application
Maissa E LLEUCH, Osman H ASAN, Sofiene TAHAR and Mohamed A BID . . . . . . . . . . . . . . . . . 43
II Session: Fault tolerance and performance evaluation 59
Dynamic Feasibility Windows Reconfiguration For a Failure-Tolerant PFair Scheduling
Yves M OUAFO T CHINDA, Annie G ENIET-C HOQUET and Gaëlle L ARGETEAU -S KAPIN . . . . . . . . . 61
On the Modeling and Performance Evaluation of Cloud Computing Centers Using M/G/c/c+r
Queuing System
Assia O UTAMAZIRT, Mohamed E SCHEIKH, Djamil A ÏSSANI, Kamel B ARKAOUI and Ouiza L EKADIR . 77
Performance Study of Frame Aggregation Mechanisms in the New Generation WiFi
Mohand YAZID, Louiza B OUALLOUCHE -M EDJKOUNE and Djamil A ÏSSANI . . . . . . . . . . . . . . . 85
Using Model-Checking Techniques for Diagnosability Analysis of Intermittent Faults - A Railway Case-
Study
Abderraouf B OUSSIF and Mohamed G HAZEL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
III Session: Model-checking & test 105
Specifying Weak Memory Consistency with Temporal Logic
Maximilian S ENFTLEBEN and Klaus S CHNEIDER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
A Model Based Approach to Combine Load and Functional Tests for Service Oriented Architectures
Afef J MAL M AALEJ and Moez K RICHEN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
Relative Correctness: A Bridge Between Proving and Testing
Wided G HARDALLOU, Nafi D IALLO and Ali M ILI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
IV Session: Protocols and distrubuted systems 157
Petri Net Synthesis from Labelled Transition Systems and from Languages (Invited talk)
Eric B ADOUEL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159
ePassport Protocol on the Spi Calculus
Safa S AOUDI, Souheib Y OUSFI and Riadh R OBBANA . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
Model-based Design and Formal Analysis of Arbitration Protocols on Multiple-Bus Architecture
Imene B ENHAFAIEDH and Maroua B EN S LIMANE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
5
CONTENTS
Towards correct Evolution of Conversation Protocols
Sarah B ENYAGOUB, Meriem O UEDERNI and Yamine A IT A MEUR . . . . . . . . . . . . . . . . . . . . . 193
6