Deriving correct distributed system designs from global requirements

从全局需求中得出正确的分布式系统设计

• 批准号: RGPIN-2016-03717
• 负责人: Bochmann, Gregor
• 金额: $ 2.26万
• 依托单位: University of Ottawa
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=683812
• 关键词: Deriving; correct; distributed; system; designs

The general theme of the proposal is the development of distributed system designs that are correct by construction for applications in the current and future e-society and for cyber-physical systems. Most applications involve communication: between humans (telephony and teleconferencing), between humans and computers (typical Web applications, e-shopping, video on demand, and broadcasting), or between several computers (distributed automated business processes, production control or semi-automatic cars sharing the road). These applications are realized using distributed databases, computers, smart phones, and many other devices; and they require complex software for controlling the interactions between these different components.***During the system and software development process for distributed systems, the development of the overall system design is critical for correctness, performance and reliability. The objective of the proposed research is the improvement of methods and tools that can be used to obtain a correct design specification for distributed systems semi-automatically by deriving the design specification from the global system requirements. Traditionally, distributed system design is very error-prone; moreover, testing a distributed system for reliability is very complex. Through an appropriate derivation algorithm, one can obtain a distributed system specification that is correct by construction.***For deriving distributed design specifications semi-automatically, we will follow two different paradigms that apply in different situations:***1. Protocol derivation: In this case, the protocol of message exchanges between the different system components is derived from the global behavior specification which defines the order of actions to be performed by the different system components. ***2. Controller derivation: In this case, the behavior of the “plant” is given, as well as the inputs from the “environment”, and the problem is to define the behavior of a “controller” that interacts with the plant and the environment in such a way that the behavior of the plant is restricted such that a desirable “control objective” is satisfied. ***We plan to develop algorithms that can be used for these two approaches for finding correct distributed system designs, to build tools that implement these algorithms, and to apply these approaches to practical applications in order to demonstrate the usefulness of the proposed system development approaches. Through such practical experiments, we expect to identify points for further improvements and obtain proofs of concepts.*** ***We expect that the developed methods and tools will be useful to the Canadian software industry for the development of distributed applications in the fields of social networks, e-society and cyber-physical systems.********

该提案的总主题是发展分布式系统设计，这些设计通过构建在当前和未来的电子社会以及网络物理系统中的应用是正确的。大多数应用程序涉及通信：人与人之间(电话和电话会议)、人与计算机之间(典型的Web应用程序、电子购物、视频点播和广播)，或者几台计算机之间(分布式自动化业务流程、生产控制或共享道路的半自动汽车)。这些应用是使用分布式数据库、计算机、智能手机和许多其他设备来实现的；它们需要复杂的软件来控制这些不同组件之间的交互。*在分布式系统的系统和软件开发过程中，总体系统设计的开发对于正确性、性能和可靠性至关重要。这项研究的目的是改进方法和工具，通过从全局系统需求导出设计规范，半自动地获得正确的分布式系统设计规范。传统上，分布式系统设计非常容易出错；而且，测试分布式系统的可靠性非常复杂。通过适当的派生算法，可以通过构造获得正确的分布式系统规范。*为了半自动地派生分布式设计规范，我们将遵循两种不同的范型，适用于不同的情况：*1.协议派生：在这种情况下，不同系统组件之间的消息交换协议是从定义不同系统组件执行的操作顺序的全局行为规范派生出来的。*2.控制器派生：在这种情况下，给出“对象”的行为以及来自“环境”的输入，问题是定义与对象和环境相互作用的“控制器”的行为，使对象的行为受到限制，从而满足期望的“控制目标”。*我们计划开发可用于这两种方法的算法，以找到正确的分布式系统设计，构建实现这些算法的工具，并将这些方法应用于实际应用，以证明所提出的系统开发方法的有效性。通过这样的实际实验，我们希望能找出需要进一步改进的地方，并获得概念的证明。*我们期望所开发的方法和工具将对加拿大软件业在社交网络、电子社会和网络物理系统领域开发分布式应用程序有所帮助。*