=Paper=
{{Paper
|id=Vol-1431/preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1431/preface.pdf
|volume=Vol-1431
}}
==None==
https://ceur-ws.org/Vol-1431/preface.pdf
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