| In this thesis, I investigate the applicability of formal methods, such as process algebras, finite state machines and temporal logics, to specify, simulate and verify complex systems, including Agent Interaction Protocols (AIPs) and Constraint Satisfaction Problems (CSPs).; Interaction is the most important characteristic of multi-agent systems. I propose here a unifying Lotos-based framework that provides a generic, reusable agent architecture as well as a methodology to construct and refine AIP specifications in an incremental way. The proposed framework also facilitates formal validation and verification of AIP specifications using rigorous tools. I also investigate the approach of using Lotos to describe agent interaction in different abstraction levels. Hence, the proposed framework can describe almost all aspects of agent interaction in different abstraction levels. In addition, I demonstrate how to generate an online auction-protocol from the generic framework, and how to simulate and verify this protocol.; CSPs are used to solve a large variety of combinatorial problems. In fact, it may be difficult to transform arbitrary problems into CSPs. Therefore, I ease the description of CSPs by providing a generic Lotos library and template. Indeed, Lotos provides an ideal level of abstraction for clearly and correctly describing CSPs. In addition, I have significantly improved the speed of model-checking for finding solutions to CSP Lotos specifications through CSP techniques, for instance, Arc-Consistency, Look-Ahead and Forward-Checking algorithms. |
