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.

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