@article {Talbi2020448,
	title = {A cloud broker architecture for cloud service selection based on multi-criteria decision making and rough set theory},
	journal = {International Journal of Computer Aided Engineering and Technology},
	volume = {13},
	number = {4},
	year = {2020},
	note = {cited By 2},
	pages = {448-464},
	abstract = {Cloud computing is a rising field providing computation resources. It represents a new paradigm of utility computing and enormously growing phenomenon in the present IT industry and economy hype. The companies which provide services to customers are called as cloud service providers. The cloud users (CUs) increase and require secure, reliable and trustworthy cloud service providers (CSPs) from the market. So, it{\textquoteright}s a challenge for a new user to choose the best provider. In this paper, we propose cloud broker architecture to help a new customer to find out the best CP. This architecture is based on a combination of rough set theory and multi-criteria analysis of some parameters related to the quality of service of the available providers. A mathematical model is used to do this analysis; it integrates multi-Agent systems to present an intelligent, distributed and collaborative method in order to add assistance to each actor in cloud computing environment. {\textcopyright} 2020 Inderscience Enterprises Ltd.. All rights reserved.},
	doi = {10.1504/IJCAET.2020.110481},
	url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-85094668160\&doi=10.1504\%2fIJCAET.2020.110481\&partnerID=40\&md5=648ac741f4e3dd89be572212f2de2586},
	author = {Talbi, J. and Haqiq, A.}
}
@conference {Haqiq2018264,
	title = {Towards integration of fault tolerance in agent-based systems},
	booktitle = {Procedia Computer Science},
	volume = {127},
	year = {2018},
	pages = {264-273},
	doi = {10.1016/j.procs.2018.01.122},
	url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-85045687698\&doi=10.1016\%2fj.procs.2018.01.122\&partnerID=40\&md5=45d788bfaa02c77cfb9b21c35098cf5d},
	author = {Haqiq, A. and Bounabat, B.}
}
@conference {Haqiq201742,
	title = {Using BECAMEDA method to specify and verify a smart home system},
	booktitle = {ACM International Conference Proceeding Series},
	volume = {Part F130526},
	year = {2017},
	note = {cited By 0},
	pages = {42-47},
	abstract = {Designing a correct model for smart systems requires an accurate specification and verification prior to development. This paper proposes the use of BECAMEDA (Behavioral SpEcification and VerifiCAtion of RMAS based on E-MDRA) method, which helps the designer predicting the system behaviour, and verifying the relevant behaviour of the system properties. BECAMEDA method is based on Multi-Agent concept and formal method, and it proposes an iterative process consisted of four phases: identification, definition, modelling and verification, to help understanding the system starting from goals identification that captures the system needs, and ending with a formal verification of the system properties. The proposed method is illustrated with an example of a Smart Home System1. {\textcopyright} 2017 Copyright is held by the owner/author(s).},
	doi = {10.1145/3128128.3128135},
	url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-85030309106\&doi=10.1145\%2f3128128.3128135\&partnerID=40\&md5=41be1e2c80793b0eb4a66d538b1df778},
	author = {Haqiq, A. and Bounabat, B.}
}
@conference {Haqiq2016329,
	title = {An extended approach for the behavioral and temporal constraints specification of reactive agent},
	booktitle = {International Conference on Intelligent Systems Design and Applications, ISDA},
	volume = {2016-June},
	year = {2016},
	note = {cited By 1},
	pages = {329-334},
	abstract = {Reactive Muti-Agent System (RMAS) provides efficient mechanism for modeling, decision-making and problem solving for complex systems. However, there is a crucial lack concerning building a specification method facilitating the designer to take into account the fundamental properties of reactive systems, which are concurrency, temporal constraints and reliability. This paper proposes to extend the Multi Decisional Reactive Agent (MDRA) approach, which is mainly focusing on reactive system, by providing mechanisms to specify temporal constraints as well as three operations mode in agent behavior, namely, normal, degraded and full-fault tolerance. {\textcopyright} 2015 IEEE.},
	doi = {10.1109/ISDA.2015.7489249},
	url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-84978405415\&doi=10.1109\%2fISDA.2015.7489249\&partnerID=40\&md5=897235a75cd05f7bf6894f33057a8343},
	author = {Haqiq, A. and Bounabat, B.}
}
@conference {Haqiq2015,
	title = {Towards an approach for behavioral specification of reactive multi-agent system},
	booktitle = {2015 5th International Conference on Information and Communication Technology and Accessibility, ICTA 2015},
	year = {2015},
	note = {cited By 0},
	abstract = {Reactive Multi-Agent system (RMAS) has emerged as an attractive technology for the design and implementation of distributed and cooperative systems. The RMAS main challenge is how to clearly identify its local and global behavior. Several approaches have been introduced to deal with behavioral specification of RMAS. However, there is a lack in the specification and verification process that facilitates understanding the system from goals identification that the system expects to achieve to formal verification of system properties. In this paper, we are interested to the specification problem of Reactive Multi-Agent System (RMAS) for both individual and collective behavior by taking into account two modes of specification: normal mode and fault-tolerance mode. To do so, we propose a method called BECAMEDA (Behavioral SpEcification and VerifiCAtion of RMAS based on E-MDRA) for the specification and verification of reactive Multi-agent system based on the MDRA (Multi-Decisional Reactive Agent) models. The MDRA specifies the reactive agent behavior by highlighting the decisional aspect of the agent. The BECAMEDA method will be described throughout an example of Car Crisis Management. {\textcopyright} 2015 IEEE.},
	doi = {10.1109/ICTA.2015.7426924},
	url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-84988311281\&doi=10.1109\%2fICTA.2015.7426924\&partnerID=40\&md5=b90071d788aab87fd79309f12b99b1bf},
	author = {Haqiq, A. and Bounabat, B.}
}
@conference {Haqiq2013,
	title = {Verification of multi decisional reactive agent using SMV model checker},
	booktitle = {2013 8th IEEE Design and Test Symposium, IDT 2013},
	year = {2013},
	note = {cited By 0},
	abstract = {On account of the evolution of technology, more complicated software arrives with the need to be verified to prevent the errors occurrence in a system which could generate fatal accidents and economic loss. These errors must be detected in an early stage during the development process to reduce redesign costs and faults. To ensure the correctness of software systems, formal verification provides an alternative approach to verify that an implementation of the expected system fulfills its specification. This paper focuses on the verification of reactive system behaviors specified by the Multi Decisional Reactive Agent (MDRA) and modeled using MDRA Profile. The objective in this paper is to use the Model Checking technique for MDRA Profile verification through the Model Checker SMV (Symbolic Model Verifier) to automatically verify the system properties expressed in temporal logic. The SMV mainly focusing on reactive systems provides a modular hierarchical descriptions and definition of reusable components. Besides, the expression of system properties is more described through both Computational Tree Logic (CTL) and Linear Temporal Logic (LTL). {\textcopyright} 2013 IEEE.},
	doi = {10.1109/IDT.2013.6727075},
	url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-84894438200\&doi=10.1109\%2fIDT.2013.6727075\&partnerID=40\&md5=f9d391f76523ab3cbdb7727b864f5e91},
	author = {Haqiq, A. and Bounabat, B.}
}
