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

SHF：小型：协作研究：分布式交互的形式分析

• 批准号: 1117708
• 负责人: Tevfik Bultan
• 金额: $ 32.86万
• 依托单位: University of California-Santa Barbara
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-10-01 至 2016-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1117708&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Formal

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.

并发和分布式软件系统可靠性的一个至关重要的问题，这些系统在以服务为导向的体系结构，云计算，多核硬件的进展中变得普遍，是构成整个系统的不同组件的协调。为了完成任务，软件系统的组件必须通过相互交互来协调其执行。基于介绍的通信是一种越来越常见的交互机制，用于并发和分布式系统中，其中组件通过发送和接收消息相互交互。拟议研究的目的是开发用于基于消息的交互的规范，分析和验证的新技术。拟议的研究将开发沟通合同规范模型的层次结构，并研究每个类别的分析和验证问题。在提议的框架内，软件系统组件之间的交互（称为对等）将被建模为描述同行之间交换消息的全局序列的对话。拟议的研究将导致一个工具集，用于分析通信合同并验证一组遵循agiven通信合同的同行产生的对话的属性。 这项研究将在至少三个领域产生更大的影响。通过开发用于分析和验证并发和分布式系统中基于消息的交互的技术，该研究将改善软件系统在各种应用领域（包括电子商务，消费者应用程序和电信）中的可靠性。其次，研究活动将有助于通过各种教育活动，包括课程，研讨会和个人研究指导，使研究生和本科生在并发和分布式系统以及基于消息的沟通中的分析和验证问题。最后，研究活动将有助于传播开发的知识，技术和工具，以通过在开放文献中发布来分析和验证通信系统，并使软件工具在公共领域中可用。