@conference { ISI:000360095400010, title = {A Formal Modeling Approach for Emergency Crisis Response in Health during Catastrophic Situation}, booktitle = {INFORMATION SYSTEMS FOR CRISIS RESPONSE AND MANAGEMENT IN MEDITERRANEAN COUNTRIES}, series = {Lecture Notes in Business Information Processing}, volume = {196}, year = {2014}, note = {1st International Conference on Information Systems for Crisis Response and Management in Mediterranean Countries (ISCRAM-Med), Toulouse, FRANCE, OCT 15-17, 2014}, pages = {112-119}, publisher = {ISCRAM Assoc; IRIT Lab Toulouse; Univ Toulouse; Univ Lorraine; Ecole Mines Albi Carmaux}, organization = {ISCRAM Assoc; IRIT Lab Toulouse; Univ Toulouse; Univ Lorraine; Ecole Mines Albi Carmaux}, abstract = {The EMS (Emergency Medical Services: {\textquoteleft}{\textquoteleft}SAMU{{\textquoteright}{\textquoteright}}), which is affiliated to the Moroccan Ministry of Health, is normally dedicated to coordinate, regulate and carry the sick and road casualty to the most suitable hospital facilities. In times of crisis, the EMS (SAMU) collaborates and coordinates with other stakeholders namely Civil Protection and Military health services by setting up advanced Medical positions (PMA). In this work we will focus mainly on the collaborative work between doctors and the EMS (SAMU) in order to provide a remote diagnosis during emergency situations. One objective of this paper is to formally specify the behavior of different components of a collaborative system architecture in telemedicine. The objective of these formal specifications is to increase the confidence in the collaborative architecture and to verify the consistency of the components assembly. This is important towards building a robust system free from specification errors and inconsistencies.}, isbn = {978-3-319-11817-8}, issn = {1865-1348}, author = {Ouzzif, Mohammed and Hamdani, Marouane and Mountassir, Hassan and Erradi, Mohammed}, editor = {Hanachi, C and Benaben, F and Charoy, F} } @article { ISI:000256710200013, title = {Description of a teleconferencing floor control protocol and its implementation}, journal = {ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE}, volume = {21}, number = {3}, year = {2008}, note = {6th Conference on Modelling and Simulation, Rabat, MOROCCO, 2006}, month = {APR}, pages = {430-441}, abstract = {In this paper, we present a formal specification of a teleconferencing floor control protocol and its implementation. The services provided by this protocol are described within the SCCP IETF document (Simple Conference Control Protocol). Finite state machines are used to model services behaviours part of this protocol. Temporal properties are defined as constraints of the teleconferencing system using SCCP protocol. The dynamic properties are described by the LTL logic (Linear Temporal Logic) and verified using the model-checker Spin/Promela. A prototype of a multimedia teleconferencing system is implemented and it is based on the specified protocol. This implementation uses UML notation and is developed with JMF (Java Media Framework) API. (C) 2007 Elsevier Ltd. All rights reserved.}, issn = {0952-1976}, doi = {10.1016/j.engappai.2007.11.003}, author = {Ouzzif, Mohammed and Erradi, Mohammed and Mountassir, Hassan} }