Belgacem B EN H EDIA, CEA, LIST, France Florin Popentiu V LADICESCU, University of Oradea, Romania VECoS’2015 Verification and Evaluation of Computer and Communication Systems 9th International Workshop Bucharest, Romania, September 10-11, 2015 Proceedings c Copyright 2015 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 1431 at CEUR Workshop Proceedings ISSN 1613-0073 http://ceur-ws.org/Vol-1431 PREFACE These are the proceedings of the 9th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS’2015) held the 10th and 11th of September 2015 at the University POLITEHNICA of Bucharest that is the main organizer together with the support of MeFoSyLoMa group and Formal Methods Europe. The International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS) was created by an Euro-Maghrebian 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 and VECoS 2014 in Bejaia. 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 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, and 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: Liliana C UCU -G ROSJEAN from AOSTE, INRIA Paris-Rocquencourt, France, Gabriel C IOBANU from Romanian Academy, ICS, Iasi, Romania and Mohamed K A ÂNICHE from LAAS, Toulouse, France. We received 15 high-quality contributions. For each paper three to five reviews were made. The program committee has accepted 9 papers for full presentation. Without support of our academic and corporate sponsors, the enormous efforts of authors, reviewers, steering committee and the local organizational team this workshop wouldn’t provide such an interesting booklet. We thank the authors for their submissions and the program committee for their hard work. September 2015 Belgacem B EN H EDIA and Florin Popentiu V LADICESCU 3 ORGANIZING COMMITTEE Professor Nicolae Tăpus, Computer Science Department, The Faculty of Automatic Control and Computer Science, University POLITEHNICA of Bucharest, Bucharest, Romania Professor Viorel-Puiu Paun, Faculty of Applied Sciences, University POLITEHNICA of Bucharest, Bucharest, Romania STEERING COMMITTEE Hassane Alla , GIPSA Lab INPG Grenoble Djamil Aissani, LAMOS, Université de Bejaia Kamel Barkaoui , CEDRIC CNAM Paris (Chair) Hanifa Boucheneb, Veriform, Ecole Polytechnique de Montréal Francesco Flammini, Ansaldo STS, Milano Mohamed Kaaniche, LAAS CNRS, Toulouse Bruno Monsuez , ENSTA - UIIS, Paris Nihal Pekergin , LACL UPEC, Créteil Denis Poitrenaud, LIP6 UPMC, Paris Tayssir Touili, LIAFA, Université Paris Diderot PROGRAM COMMITTEE Bernhard K. Aichernig, ISF, Graz Mohamed Jmaı̈el, ENSI, Sfax Djamil Aissani, LAMOS, Bejaia Mohamad Jaber, AUB, Beyrouth Yamine Ait Ameur, IRIT/ENSEEIHT, Toulouse Jorge Julvez, University of Zaragoza Otmane Ait Mohamed, Concordia University, Montréal Mohamed Kaaniche, LAAS, Toulouse Hassane Alla, GIPSA, Grenoble Lars Michael Kristensen, Bergen Univ. College, Bergen Lamia Atma Djoudi, Synchrone Technologies, Paris Bechir Ktari, Université Laval, Québec Kamel Barkaoui, Cedric Cnam, Paris Gaiyun Liu, Xidian Univ., Xi’an Zohra Bakkoury, EMI EAMPIS, Rabat Borhen Marzougui, ECT, Abu Dhabi Belgacem Ben Hedia, LIST-CEA, Saclay (co-chair) Mourad Maouche, Philadephia University, Amman Saddek Bensalem, VERIMAG Grenoble, France Louiza Bouallouche Medjkoune, LAMOS, Bejaia Simon Bliudze, EPFL, Lausanne Bruno Monsuez, ENSTA ParisTech, Saclay Jean-Louis Boimond, LARIS, Angers Mohamed Mosbah, LaBRI, Bordeaux Patrice Bonhomme, LI, Tours Safia Nait-Bahloul, LITIO, Université d’Oran Abdelmadjid Bouabdallah, Heudiasyc Lab, Compiegne Meriem Ouederni, IRIT, Toulouse Hanifa Boucheneb, Polytechnique Montréal Claire Pagetti, ONERA, Toulouse Florian Brandner, ENSTA ParisTech, Saclay Vladimir Paun, ENSTA ParisTech, Palaiseau Carla Ceatzu, University of Cagliari Nihal Pekergin, LACL, Créteil Tijani Chahed, Telecom SudParis, Evry Olivier Perrin, INRIA-LORIA, Nancy Feng Chu, IBISC, Evry Denis Poitrenaud, LIP6, Paris Isabel Demongodin, LSIS Marseille Florin Popentiu Vladicescu, Univ. of Oradea (co-chair) Josée Desharnais, Université Laval, Quebec Riadh Robbana, INSAT, Tunis Karim Djouani, LISSI UPEC, Créteil Zaı̈di Sahnoun, LIRE, Constantine Mohamed Escheikh, ENIT,Tunis Zohra Sbaı̈, ENIT, Tunis Alessandro Fantecchi, Unifi, Italy Larbi Sekhri, Univ. es Senia, Oran Francesco Flammini, Ansaldo STS, Milano Nadia Tawbi, Université Laval, Quebec Mohamed Ghazel, INRETS, Villeneuve d’Ascq Thouraya Tebibel, ESI, Alger Latéfa Ghomri, University of Tlemcen. Ferucio Laurentiu Tiplea, University of Iasi Bernd Heidergott, VU Amsterdam University Tayssir Touili, LIPN Villetaneuse Serge Haddad, LSV Cachan Farouk Toumani, LIMOS, Clermont-Ferrand Awatef Hicheur Cairns, Altran Research, Velizy Karsten Wolf, Universitaet Rostock Malika Ioulalen, USTHB Alger 4 CONTENTS I Session: Control and Diagnosis 7 Resilience Assessment: Accidental and Malicious Threats (Invited talk) Mohamed K A ÂNICHE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Fault Diagnosis of P-Time Labeled Petri Net Systems Patrice B ONHOMME . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Combining Enumerative and Symbolic - Techniques for Diagnosis of Discrete-Event Systems Abderraouf B OUSSIF, Mohamed G HAZEL and Kais K LAI . . . . . . . . . . . . . . . . . . . . . . . . . . 23 II Session: Program verification 35 Probabilistic Approaches for Time Critical Embedded Systems (Invited talk) Liliana C UCU -G ROSJEAN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Towards the Property-Based Testing of an L4 Microkernel API Cosmin D RAGOMIR, Lucian M OGOSANU, Mihai C ARABAS, Razvan D EACONESCU and Nicolae TAPUS 39 An Approach for Formal Verification of Updated Java Bytecode Programs Razika L OUNAS, Mohamed M EZGHICHE and Jean-Louis L ANET . . . . . . . . . . . . . . . . . . . . . . 51 State Space Reduction Strategie for Model Checking Concurrent C Programs Amira M ETHNI, Matthieu L EMERRE, Belgacem B EN H EDIA, Serge H ADDAD and Kamel B ARKAOUI . 65 III Session: Performance evaluation 77 Timeout Interaction and Migration in Distributed Systems (Invited talk) Gabriel C IOBANU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 Model-Based Verification of the DMAMAC Protocol for Real-time Process Control Admar Ajith Kumar S OMAPPA, Andreas P RINZ and Lars K RISTENSEN . . . . . . . . . . . . . . . . . . 81 On quantitative Analysis of Time Open Workflow Nets and Parametric Extension Zohra S BA Ï and Kamel B ARKAOUI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Verification of Bounded Real-Time Distributed Systems With Mobility Bogdan A MAN and Gabriel C IOBANU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 5