SHF: Small: Collaborative Research: Formal Analysis of Distributed Interactions

随着面向服务的体系结构、云计算、多核硬件的发展，并发和分布式软件系统的可靠性中的一个关键问题是组成整个系统的不同组件的协调。为了完成一项任务，软件系统中的组件必须通过相互交互来协调它们的执行。基于消息的通信是并发和分布式系统中越来越常见的交互机制，组件之间通过发送和接收消息进行交互。这项研究的目的是开发新的技术来描述、分析和验证基于消息的交互。该研究将建立通信合同规范模型的层次结构，并调查每类的分析和验证问题。在所提出的框架内，软件系统组件(称为对等体)之间的交互将被建模为描述对等体之间交换的消息的全局序列的会话。拟议的研究将产生一个工具集，用于分析通信合同并验证由遵循已有通信合同的一组对等点生成的对话的属性。这项研究将至少在三个领域产生更广泛的影响。通过开发并发和分布式系统中基于消息的交互的分析和验证技术，这项研究将提高包括电子商务、消费者应用和电信在内的广泛应用领域中软件系统的可靠性。其次，研究活动将通过各种教育活动，包括课程、研讨会和个人研究指导，帮助研究生和本科生接触并行和分布式系统中的分析和验证问题，以及基于消息的交流。最后，研究活动将有助于传播为分析和核实通信系统而开发的知识、技术和工具，方法是在公开文献中出版，并使软件工具在公共领域可用。

A crucial problem in dependability of concurrent and distributed software systems, which have become prevalent with the advances in service-oriented architecture, cloud computing, multi-core hardware, is the coordination of different components that form the whole system. In order to complete a task, components of a software system have to coordinate their executions by interacting with each other.Message-based communication is an increasingly common interaction mechanism used in concurrent and distributed systems where components interact with each other by sending and receiving messages. The objective of the proposed research is to develop novel techniques for specification, analysis, and verification of message-based interactions.The proposed research will develop a hierarchy of communication contract specification models and investigate analysis and verification problems for each class. Within the proposed framework the interactions among components of a software system (called peers) will be modeled as conversations describing the global sequence of messages exchanged among the peers. The proposed research will result in a toolset for analyzing communication contracts and verifying properties of conversations generated by a set of peers that follow agiven communication contract. The research will have broader impact in at least three areas. By developing techniques for analysis and verification of message-based interactions in concurrent and distributed systems, the research will improve the dependability of software systems in a wide variety of application domains, including e-commerce, consumer applications, and telecommunications. Secondly, the research activity will help to expose graduate and undergraduate students to analysis and verification problems in concurrent and distributed systems, and message-based communication, through a variety of educational activities including courses, seminars and individual research mentoring. Finally, the research activity will help to disseminate the knowledge, techniques and tools developed for analysis and verification of communicating systems through publishing in the open literature, and making the software tools available in public domain.