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.