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 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 stateof-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.
Abichou Azgal, Tunisia Polytechnic School (General
Adel Benzina, Tunisia Polytechnic School (Chair) Takoua Abdellatif, Tunisia Polytechnic School
Hassane Alla, GIPSA Lab, INPG Grenoble Djamil Aissani, LAMOS, Universite´ de Bejaia Kamel Barkaoui, CEDRIC, CNAM Paris (Chair) Hanifa Boucheneb, Ecole Polytechnique de Montre´al Francesco Flammini, Ansaldo STS, Milano
Takoua Abdellatif, EPT, Tunis Djamil Aissani, LAMOS, Bejaia Hassane Alla, GIPSA, Grenoble Yamine Ait Ameur, IRIT/ENSEEIHT, Toulouse Mohamed Faouzi Atig, Uppsala University Kamel Barkaoui, Cedric Cnam, Paris Fa¨ıza Belala, LIRE, IC2, Algeria Saddek Bensalem, VERIMAG Grenoble, France Adel Benzina, LESCN-EPT, Tunis Mohamed Tahar Bhiri, ISIM, Sfax Simon Bliudze, EPFL, Lausanne Patrice Bonhomme, LI, University of Tours Fre´de´ric Boniol, ONERA, Toulouse Abdelmadjid Bouabdallah, Heudiasyc Lab, Compiegne Ahmed Bouajjani, LIAFA, Paris Hanifa Boucheneb, Ecole Polytechnique de Montre´al Mahmoud Boufaida, LIRE Univ. Constantine 2 Florian Brandner, Telecom ParisTech Awatef Hicheur Cairns, Cedric, Cnam, Paris Annie Choquet-Geniet, LISI, Ensma, Poitiers Feng Chu, IBISC, Evry Gabriel Ciobanu, Romanian Academy, ICS, Iasi Liliana Cucu-Grosjean, INRIA Paris-Rocquencourt Isabel Demongodin, LSIS Marseille Jose´e Desharnais, Universite´ Laval, Quebec Karim Djouani, LISSI UPEC, Cre´teil Lamia Atma Djoudi, Synchrone Technologies, Paris Mohammed Erradi, ENSIAS, Rabat Mohamed Escheikh, ENIT,Tunis Alessandro Fantecchi, Unifi, Italy Francesco Flammini, Ansaldo STS, Milano Fabio Gadducci, CSD, University of Pisa Mohamed Ghazel, IFSTTAR, Lille (co-chair) Khaled Ghedira, ANPR, Tunis Late´fa Ghomri, University of Tlemcen Mohamed Graiet, MIRACL, Monastir Mohand-Said Hacid , LIRIS, Lyon Serge Haddad, LSV ENS Cachan Ahmed Hadj-Kacem, ReDCAD, Sfax Imen Ben Hafaiedh, LIP2 ISI , Tunis Belgacem Ben Hedia, LIST-CEA, Saclay Bernd Heidergott, VU Amsterdam University Malika Ioulalen, USTHB Alger Mohamad Jaber, American University of Beirut Ali Jaoua, C.E, Qatar University
Bruno Monsuez, ENSTA - UIIS, Paris Nihal Pekergin, LACL UPEC, Cre´teil Denis Poitrenaud, LIP6 UPMC, Paris Tayssir Touili, LIAFA, Universite´ Paris Diderot
Exact and Approximate Diagnosis of Probabilistic Systems (Invited talk)
Serge HADDAD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Performance Evaluation of Complex Systems Using the SBIP Framework
Ayoub NOURI, Marius BOZGA, Axel LEGAY and Saddek BENSALEM . . . . . . . . . . . . . . . . . . . 11 Statistical Model Checking of CSMA/CA in WSNs
Zohra HMIDI, Laid KAHLOUL, Saber BENHARZALLAH and Cherifa OTHMANE . . . . . . . . . . . . . 27 Formal Probabilistic Analysis of Lifetime for a WSN-based Monitoring Application
Maissa ELLEUCH, Osman HASAN, Sofiene TAHAR and Mohamed ABID . . . . . . . . . . . . . . . . . 43
Dynamic Feasibility Windows Reconfiguration For a Failure-Tolerant PFair Scheduling
Yves MOUAFO TCHINDA, Annie GENIET-CHOQUET and Gae¨lle LARGETEAU-SKAPIN . . . . . . . . . 61 On the Modeling and Performance Evaluation of Cloud Computing Centers Using M/G/c/c+r Queuing System
Assia OUTAMAZIRT, Mohamed ESCHEIKH, Djamil A¨ISSANI, Kamel BARKAOUI and Ouiza LEKADIR . 77 Performance Study of Frame Aggregation Mechanisms in the New Generation WiFi
Mohand YAZID, Louiza BOUALLOUCHE-MEDJKOUNE and Djamil A¨ISSANI . . . . . . . . . . . . . . . 85 Using Model-Checking Techniques for Diagnosability Analysis of Intermittent Faults - A Railway CaseStudy
Abderraouf BOUSSIF and Mohamed GHAZEL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
Specifying Weak Memory Consistency with Temporal Logic
Maximilian SENFTLEBEN and Klaus SCHNEIDER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 A Model Based Approach to Combine Load and Functional Tests for Service Oriented Architectures
Afef JMAL MAALEJ and Moez KRICHEN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 Relative Correctness: A Bridge Between Proving and Testing
Wided GHARDALLOU, Nafi DIALLO and Ali MILI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
Petri Net Synthesis from Labelled Transition Systems and from Languages (Invited talk)
Eric BADOUEL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159 ePassport Protocol on the Spi Calculus
Safa SAOUDI, Souheib YOUSFI and Riadh ROBBANA . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 Model-based Design and Formal Analysis of Arbitration Protocols on Multiple-Bus Architecture Imene BENHAFAIEDH and Maroua BEN SLIMANE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 7 59 105 157