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 impactin 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.