Model based approach to verification of distributed and multi-agent systems

对分布式软件系统（DSS）日益增长的需求导致了几种面向代理的软件工程（ase）方法的发展。不幸的是，ose方法没有涵盖整个软件生命周期，并且通常排除了验证、监视和测试。该研究通过在需求和设计阶段检测紧急行为，为分布式系统验证提供了一种经济有效的解决方案。决策支持系统开发的一个实用方法是使用场景描述其需求。然而，基于场景的规范和基于它的行为建模容易出现一些微妙的缺陷，包括不完整和部分描述。本文主要研究了基于场景规范的多组件系统行为模型合成过程中可能出现的紧急行为。目标是自动化建模、分析、检测和解决分布式系统中的紧急行为的过程。以下研究问题将被解决：（Q1）分布式系统中紧急行为的确切原因是什么？（Q2）如何对系统进行建模和分析，以发现紧急行为？（Q3）如何发现和解决问题？可交付成果包括：(1)4步流程（即建模、分析、检测和解决），以检测决策支持系统中的紧急行为；(2)与传统的基于uml和主要的ase方法集成的软件系统，为设计验证提供无缝的支持。本研究具有坚实的理论基础和可实现的原型。通过详细的工业案例研究在各种现实领域的问题，如信息检索和分布式制造系统，我们将显示该方法的效率和有效性。本研究可以(1)提高决策支持系统的系统级安全性；(2)通过消除令人烦恼的紧急行为障碍，帮助多智能体系统（MAS）在软件行业的广泛采用；(3)可以潜在地用于在MAS模拟和数据挖掘过程中提出可能的积极紧急行为场景。

Increasing demand for Distributed software systems (DSS) has led to the development of several Agent Oriented Software Engineering (AOSE) methodologies. Unfortunately AOSE methodologies do not cover the full software life cycle and usually exclude verification, monitoring and testing. This research provides a cost effective solution to distributed system verification by detecting emergent behaviour during the requirement and design phase. A practical approach for DSS development is describing its requirements using scenarios. However, scenario-based specification and behavioural modeling based on it are prone to subtle drawbacks including incompleteness and partial description. This research is focused on the emergent behaviour that can arise when behaviour model of a system with multiple components is synthesized from its scenario-based specification. The goal is automating the process of modeling, analyzing, detecting and resolving the emergent behaviour in distributed systems. The following research questions will be addressed: (Q1) what is the exact cause of emergent behaviour in distributed systems? (Q2) How to model and analyze the system in order to find emergent behaviour? (Q3) How to detect and resolve the problem? The deliverables are: (1) a 4 step process (i.e. modeling, analysis, detection and resolution) to detect emergent behaviour in DSS; and (2) a software system that is integrated with the conventional UML-based and major AOSE methodologies to provide seamless support for design verification. The proposed research has a solid theoretical basis and an implemented prototype. Through detailed industrial case studies in various real-life domain problems such as information retrieval and distributed manufacturing systems we will show the efficiency and effectiveness of the approach. The proposed research can (1) contribute to system level safety of DSS; (2) help wide spread adoption of multi-agent systems (MAS) in software industry by removing the vexatious emergent behaviour hurdle; and (3) can potentially be used to suggest possible positive emergent behaviour scenarios during MAS simulation and data mining.