Laarej, Amine (2020) Automatic Transformation-Based Model Checking of Multi-agent Systems. Masters thesis, Concordia University.
Preview |
Text (application/pdf)
2MBLaarej_MASc_F2020.pdf - Accepted Version Available under License Spectrum Terms of Access. |
Abstract
Multi-Agent Systems (MASs) are highly useful constructs in the context of real-world software applications. Built upon communication and interaction between autonomous agents, these systems are suitable to model and implement intelligent applications. Yet these desirable features are precisely what makes these systems very challenging to design, and their compliance with requirements extremely difficult to verify. This explains the need for the development of techniques and tools to model, understand, and implement interacting MASs. Among the different methods developed, the design-time verification techniques for MASs based on model checking offer the advantage of being formal and fully automated. We can distinguish between two different approaches used in model checking MASs, the direct verification approach, and the transformation-based approach. This thesis focuses on the later that relies on formal reduction techniques to transform the problem of model checking a source logic into that of an equivalent problem of model checking a target logic.
In this thesis, we propose a new transformation framework leveraging the model checking of the computation tree logic (CTL) and its NuSMV model checker to design and implement the process of transformation-based model checking for CTL-extension logics to MASs. The approach provides an integrated system with a rich set of features, designed to support the transformation process while simplifying the most challenging and error-prone tasks. The thesis presents and describes the tool built upon this framework and its different applications. A performance comparison with MCMAS, the model checker of MASs, is also discussed.
Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering |
---|---|
Item Type: | Thesis (Masters) |
Authors: | Laarej, Amine |
Institution: | Concordia University |
Degree Name: | M.A. Sc. |
Program: | Quality Systems Engineering |
Date: | August 2020 |
Thesis Supervisor(s): | Bentahar, Jamal and Dssouli, Rachida |
ID Code: | 987078 |
Deposited By: | AMINE LAAREJ |
Deposited On: | 25 Nov 2020 15:38 |
Last Modified: | 25 Nov 2020 15:38 |
Repository Staff Only: item control page