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

对分布式软件系统(DSS)日益增长的需求导致了几种面向代理的软件工程(AOSE)方法学的发展。遗憾的是，AOSE方法并不涵盖整个软件生命周期，通常不包括验证、监控和测试。该研究通过检测需求和设计阶段的突发行为，为分布式系统验证提供了一种经济有效的解决方案。DSS开发的一种实用方法是使用场景描述其需求。然而，基于场景的规范和基于场景的行为建模往往存在不完备性和描述片面性等微妙缺陷。这项研究集中在多组件系统的行为模型从其基于场景的规范中综合出来时可能出现的行为。其目标是自动化对分布式系统中的突发行为进行建模、分析、检测和解决的过程。将讨论以下研究问题：(Q1)分布式系统中紧急行为的确切原因是什么？(Q2)如何对系统进行建模和分析，以发现紧急行为？(Q3)如何发现和解决该问题？可交付成果是：(1)4步过程(即建模、分析、检测和解决)，以检测决策支持系统中的紧急行为；(2)与传统的基于统一建模语言的方法和主要的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.