Yazar "Elwhishi, Ahmed" seçeneğine göre listele

Listeleniyor 1 - 2 / 2
  • Küçük Resim Yok
    Öğe
    Multi-valued model checking IoT and intelligent systems with commitment protocols in multi-source data environments
    (Elsevier, 2024) Alwhishi, Ghalya; Bentahar, Jamal; Elwhishi, Ahmed; Pedrycz, Witold; Drawel, Nagat
    In today's world of connectivity, various domains use different multi-sensor Internet of Things (IoT) and Intelligent Systems (IS) applications. These applications involve extensive interactions between thousands or millions of components in open environments, which challenges verifying their reliability and efficiency. This paper introduces the first investigation in verifying IoT applications and intelligent systems in multi-source data settings with multi-agent commitment protocols in uncertain or inconsistent environments. Specifically, we present original and efficient solutions for modeling and verifying these systems with conditional and unconditional commitment protocols under uncertain or inconsistent settings. We introduce 4v-CTLc and 4v-CTLcc, multi-valued logics of commitment for reasoning about inconsistency over these systems that expand 3v-CTLc and 3v-CTLcc for reasoning about uncertainty. Moreover, we introduce new reduction algorithms for reducing our multi-valued model checking problems to the two-valued ones. To implement these algorithms, we develop two new automatic verification tools. The first tool translates the multi-valued logics to CTL and automatically interacts with the NuSMV model checker. The second tool translates these logics to the two-valued versions, CTLc and CTLcc, and automatically interacts with the MCMAS+ model checker. We apply our verification approaches to a Smart Home, a Smart Hospital and a Smart Mortgage system with multi-source data as case studies using sets of properties, including safety, liveness and reachability. The experimental results obtained by the proposed multi-valued model checking techniques proved these techniques' high efficiency and applicability to modeling and verifying intelligent and autonomous multi-source data systems.
  • Küçük Resim Yok
    Öğe
    MV-Checker: A software tool for multi-valued model checking intelligent applications with trust and commitment
    (Pergamon-Elsevier Science Ltd, 2024) Alwhishi, Ghalya; Bentahar, Jamal; Elwhishi, Ahmed; Pedrycz, Witold
    Intelligent applications are highly susceptible to uncertainty and inconsistency due to the intense and intricate interactions among their autonomous components (or agents), making their verification theoretically and practically challenging. This paper presents the design and implementation of a new open -source and scalable software tool for modeling and verifying intelligent applications with commitment and trust protocols under both uncertainty and inconsistency settings, using reduction -based multi -valued model checking techniques. The proposed tool is equipped with original and novel algorithms that transform our logics of multi -valued commitment (mv-CTLC) and multi -value trust (mv-TCTL) that we recently introduced to their classical twovalued commitment (CTLC) and trust (TCTL) logic versions as well as to Computational Tree Logic (CTL). Moreover, the tool transforms the mv-CTL to CTL, and it is applicable for the classical model checking by transforming the classical logics of trust and commitment to CTL. To demonstrate the practicality and applicability of the proposed tool in real settings, we present and report experimental results over two blockchain-based applications in the healthcare domain. Finally, we provide discussions and comparisons between the proposed approaches regarding scalability and efficiency. Moreover, we provide packages of more than 11 experiments, including the ones we conduct in this paper and enhanced experiments from previous works. Our findings ensure that the proposed approaches and the software tool that implements them are highly efficient and scalable, giving accurate results under varying conditions.