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

随着对分布式软件系统（DSS）需求的不断增长，一些面向Agent的软件工程（AOSE）方法学应运而生。不幸的是，AOSE方法并不涵盖整个软件生命周期，通常不包括验证、监控和测试。这项研究提供了一个成本效益的解决方案，分布式系统验证检测紧急行为在需求和设计阶段。DSS开发的一种实用方法是使用场景描述其需求。然而，基于规范和行为建模的基础上，它很容易微妙的缺点，包括不完整性和部分描述。本研究的重点是紧急行为时，可能会出现的行为模型的多个组件的系统是从其基于规范的合成。其目标是自动化的建模，分析，检测和解决分布式系统中的紧急行为的过程。以下研究问题将得到解决：（Q1）什么是分布式系统中紧急行为的确切原因？(Q2)如何建模和分析系统，以发现紧急行为？(Q3)如何发现和解决问题？可交付成果是：（1）一个四步程序（即建模、分析、检测和解决），以检测DSS中的紧急行为;以及（2）一个软件系统，该系统与传统的基于UML的和主要的AOSE方法相结合，为设计验证提供无缝支持。该研究具有坚实的理论基础和实现原型。通过详细的工业案例研究，在各种现实生活中的领域问题，如信息检索和分布式制造系统，我们将显示的效率和有效性的方法。所提出的研究可以（1）有助于DSS的系统级安全性;（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.