Deriving correct distributed system designs from global requirements

点击翻译按钮获取中文摘要

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.********