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 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 CUCU-GROSJEAN from AOSTE, INRIA Paris-Rocquencourt, France, Gabriel CIOBANU from Romanian Academy, ICS, Iasi, Romania and Mohamed KA 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.
Professor Nicolae Ta˘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
Djamil Aissani, LAMOS, Universite´ de Bejaia Kamel Barkaoui , CEDRIC CNAM Paris (Chair) Hanifa Boucheneb, Veriform, Ecole Polytechnique de Montre´al Francesco Flammini, Ansaldo STS, Milano Mohamed Kaaniche, LAAS CNRS, Toulouse Bruno Monsuez , ENSTA - UIIS, Paris Nihal Pekergin , LACL UPEC, Cre´teil Denis Poitrenaud, LIP6 UPMC, Paris Tayssir Touili, LIAFA, Universite´ Paris Diderot
Djamil Aissani, LAMOS, Bejaia Yamine Ait Ameur, IRIT/ENSEEIHT, Toulouse Otmane Ait Mohamed, Concordia University, Montre´al Hassane Alla, GIPSA, Grenoble Lamia Atma Djoudi, Synchrone Technologies, Paris Kamel Barkaoui, Cedric Cnam, Paris Zohra Bakkoury, EMI EAMPIS, Rabat Belgacem Ben Hedia, LIST-CEA, Saclay (co-chair) Saddek Bensalem, VERIMAG Grenoble, France Simon Bliudze, EPFL, Lausanne Jean-Louis Boimond, LARIS, Angers Patrice Bonhomme, LI, Tours Abdelmadjid Bouabdallah, Heudiasyc Lab, Compiegne Hanifa Boucheneb, Polytechnique Montre´al Florian Brandner, ENSTA ParisTech, Saclay Carla Ceatzu, University of Cagliari Tijani Chahed, Telecom SudParis, Evry Feng Chu, IBISC, Evry Isabel Demongodin, LSIS Marseille Jose´e Desharnais, Universite´ Laval, Quebec Karim Djouani, LISSI UPEC, Cre´teil Mohamed Escheikh, ENIT,Tunis Alessandro Fantecchi, Unifi, Italy Francesco Flammini, Ansaldo STS, Milano Mohamed Ghazel, INRETS, Villeneuve d’Ascq Late´fa Ghomri, University of Tlemcen.
Bernd Heidergott, VU Amsterdam University Serge Haddad, LSV Cachan Awatef Hicheur Cairns, Altran Research, Velizy Malika Ioulalen, USTHB Alger
Mohamad Jaber, AUB, Beyrouth Jorge Julvez, University of Zaragoza Mohamed Kaaniche, LAAS, Toulouse Lars Michael Kristensen, Bergen Univ. College, Bergen Bechir Ktari, Universite´ Laval, Que´bec Gaiyun Liu, Xidian Univ., Xi’an Borhen Marzougui, ECT, Abu Dhabi Mourad Maouche, Philadephia University, Amman Louiza Bouallouche Medjkoune, LAMOS, Bejaia Bruno Monsuez, ENSTA ParisTech, Saclay Mohamed Mosbah, LaBRI, Bordeaux Safia Nait-Bahloul, LITIO, Universite´ d’Oran Meriem Ouederni, IRIT, Toulouse Claire Pagetti, ONERA, Toulouse Vladimir Paun, ENSTA ParisTech, Palaiseau Nihal Pekergin, LACL, Cre´teil Olivier Perrin, INRIA-LORIA, Nancy Denis Poitrenaud, LIP6, Paris Florin Popentiu Vladicescu, Univ. of Oradea (co-chair) Riadh Robbana, INSAT, Tunis Za¨ıdi Sahnoun, LIRE, Constantine Zohra Sba¨ı, ENIT, Tunis Larbi Sekhri, Univ. es Senia, Oran Nadia Tawbi, Universite´ Laval, Quebec Thouraya Tebibel, ESI, Alger Ferucio Laurentiu Tiplea, University of Iasi Tayssir Touili, LIPN Villetaneuse Farouk Toumani, LIMOS, Clermont-Ferrand Karsten Wolf, Universitaet Rostock
Resilience Assessment: Accidental and Malicious Threats (Invited talk)
Mohamed KA AˆNICHE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Fault Diagnosis of P-Time Labeled Petri Net Systems
Patrice BONHOMME . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Combining Enumerative and Symbolic - Techniques for Diagnosis of Discrete-Event Systems
Abderraouf BOUSSIF, Mohamed GHAZEL and Kais KLAI . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Probabilistic Approaches for Time Critical Embedded Systems (Invited talk)
Liliana CUCU-GROSJEAN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Towards the Property-Based Testing of an L4 Microkernel API
Cosmin DRAGOMIR, Lucian MOGOSANU, Mihai CARABAS, Razvan DEACONESCU and Nicolae TAPUS 39 An Approach for Formal Verification of Updated Java Bytecode Programs
Razika LOUNAS, Mohamed MEZGHICHE and Jean-Louis LANET . . . . . . . . . . . . . . . . . . . . . . 51 State Space Reduction Strategie for Model Checking Concurrent C Programs
Amira METHNI, Matthieu LEMERRE, Belgacem BEN HEDIA, Serge HADDAD and Kamel BARKAOUI . 65
Timeout Interaction and Migration in Distributed Systems (Invited talk)
Gabriel CIOBANU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 Model-Based Verification of the DMAMAC Protocol for Real-time Process Control
Admar Ajith Kumar SOMAPPA, Andreas PRINZ and Lars KRISTENSEN . . . . . . . . . . . . . . . . . . 81 On quantitative Analysis of Time Open Workflow Nets and Parametric Extension
Zohra SBA¨I and Kamel BARKAOUI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Verification of Bounded Real-Time Distributed Systems With Mobility
Bogdan AMAN and Gabriel CIOBANU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109