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

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

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.