Automated Construction of Dependable Component-based Cyber-physical Models

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

A cyber-physical system (CPS) is a system in which there is a tight conjoining between computational and physical resources. Examples of such a system include autonomous collision avoidance systems, medical devices, autonomous search and rescue devices, and avionics systems. It is expected that the role of these systems will expand significantly in the near future. To realize this potential, future CPSs will need to be correct and significantly more efficient and dependable. These objectives introduce numerous challenges. For example, we currently lack formal methods for specifying and reasoning about the correctness of CPSs. Moreover, it is unclear how constraints in a CPS's environment affect widely understood notions such as correctness, fault-tolerance, maintenance, and separation of concerns. In this proposal, I advocate the approach of developing model-based methods that automatically build CPSs that are correct by construction. Model-based application development aims at increasing the integrity by using models employed in clearly defined transformation steps leading to correct-by-construction artifacts. In particular, I would argue that CPSs are inherently component-based, as physical and computational processes are normally stand-alone entities communicating with each other. Thus, this research program will focus on model-based development of fault-tolerant component-based CPSs. Specifically, the outcome of this project will be (1) a simple, intuitive, and yet expressive framework for formal modeling of component-based CPSs, (2) rigorous complexity analysis of automated formal methods for adding fault-tolerance to a fault-intolerant component-based model of a CPS, (3) transformation methods that separate fault-tolerance from functional concerns and sufficient conditions for compositional synthesis of CPSs, and (4) a powerful tool chain that realizes the theoretical results in practice.