Cyber-physical systems (CPS), such as cars and robots, are pervasive in our modern society. As CPS consist of heterogeneous components, analysis of such systems requires knowledge from different domains, such as mechanics, software engineering, control theory, and most recently artificial intelligence. However, practitioners and researchers of CPS lack a versatile framework that supports modelling all kinds of components in CPS and provides suitable verification and synthesis methods. The author proposes such a modelling framework and its implementation in this paper. This framework employs various formalisms to model the physical processes, controlling software, and external environment of CPS. The implementation of the framework is realised in UPPAAL, which supports symbolic and statistical model checking, as well as controller synthesis. This framework provides experts from different domains with analytical methods on both individual components and the entire system such that they can comprehensively consider the mutual influence of their design decisions. A case study of motion planning for autonomous vehicles demonstrates the applicability and versatility of the framework.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Modelling Cyber-Physical Systems for Verification and Synthesis

  • Rong Gu

摘要

Cyber-physical systems (CPS), such as cars and robots, are pervasive in our modern society. As CPS consist of heterogeneous components, analysis of such systems requires knowledge from different domains, such as mechanics, software engineering, control theory, and most recently artificial intelligence. However, practitioners and researchers of CPS lack a versatile framework that supports modelling all kinds of components in CPS and provides suitable verification and synthesis methods. The author proposes such a modelling framework and its implementation in this paper. This framework employs various formalisms to model the physical processes, controlling software, and external environment of CPS. The implementation of the framework is realised in UPPAAL, which supports symbolic and statistical model checking, as well as controller synthesis. This framework provides experts from different domains with analytical methods on both individual components and the entire system such that they can comprehensively consider the mutual influence of their design decisions. A case study of motion planning for autonomous vehicles demonstrates the applicability and versatility of the framework.