首页> 外文学位 >Model Based Safety Analysis and Verification of Cyber-Physical Systems.
【24h】

Model Based Safety Analysis and Verification of Cyber-Physical Systems.

机译:基于模型的网络物理系统安全性分析和验证。

获取原文
获取原文并翻译 | 示例

摘要

Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software safety in CPSes, to avoid hazards to property and human life as a result of un-controlled interactions, is essential and challenging. The principal hurdle in this regard is the characterization of the context driven interactions between software and the physical environment (cyber-physical interactions), which introduce multi-dimensional dynamics in space and time, complex non-linearities, and non-trivial aggregation of interaction in case of networked operations.;Traditionally, CPS software is tested for safety either through experimental trials, which can be expensive, incomprehensive, and hazardous, or through static analysis of code, which ignore the cyber-physical interactions. This thesis considers model based engineering, a paradigm widely used in different disciplines of engineering, for safety verification of CPS software and contributes to three fundamental phases: a) modeling, building abstractions or models that characterize cyberphysical interactions in a mathematical framework, b) analysis, reasoning about safety based on properties of the model, and c) synthesis, implementing models on standard testbeds for performing preliminary experimental trials.;In this regard, CPS modeling techniques are proposed that can accurately capture the context driven spatio-temporal aggregate cyber-physical interactions. Different levels of abstractions are considered, which result in high level architectural models, or more detailed formal behavioral models of CPSes. The outcomes include, a well defined architectural specification framework called CPS-DAS and a novel spatio-temporal formal model called Spatio-Temporal Hybrid Automata (STHA) for CPSes.;Model analysis techniques are proposed for the CPS models, which can simulate the effects of dynamic context changes on non-linear spatio-temporal cyberphysical interactions, and characterize aggregate effects. The outcomes include tractable algorithms for simulation analysis and for theoretically proving safety properties of CPS software.;Lastly a software synthesis technique is proposed that can automatically convert high level architectural models of CPSes in the healthcare domain into implementations in high level programming languages. The outcome is a tool called Health-Dev that can synthesize software implementations of CPS models in healthcare for experimental verification of safety properties.
机译:医疗保健,电力系统和Web服务中的关键基础架构包含了网络物理系统(CPS),其中软件控制的计算系统通过启动和监视与物理环境进行交互。确保CPS中的软件安全,避免由于不受控制的交互作用而对财产和人类生命造成危害,这是至关重要且具有挑战性的。在这方面的主要障碍是表征软件与物理环境之间的上下文驱动的交互(网络-物理交互),这会引入时空的多维动态,复杂的非线性以及交互的非平凡聚合传统上,CPS软件会通过可能昂贵,不全面且危险的实验性试验或通过忽略网络物理交互的代码静态分析来进行安全性测试。本文考虑了基于模型的工程(一种广泛用于不同工程学科的范式)来验证CPS软件的安全性,并致力于三个基本阶段:a)在数学框架中建模,构建抽象化或表征网络物理相互作用的模型; b)分析,根据模型的性质进行安全性推理,以及c)合成,在标准试验台上实施模型以进行初步的实验性试验。在这方面,提出了CPS建模技术,可以准确地捕获上下文驱动的时空聚合网络身体上的互动。考虑了不同级别的抽象,这导致了高级体系结构模型或更详细的CPS正式行为模型。结果包括一个定义明确的体系结构规范框架CPS-DAS和一个新颖的时空形式化模型CPSes的时空混合自动机(STHA).CPS模型提出了模型分析技术,可以模拟效果动态情境变化对非线性时空网络物理相互作用的影响,并表征聚集效应。结果包括用于仿真分析和从理论上证明CPS软件安全特性的易处理算法。最后,提出了一种软件综合技术,该技术可以将医疗保健领域的CPS的高级体系结构模型自动转换为高级编程语言的实现。结果是一个名为Health-Dev的工具,该工具可以综合医疗保健中CPS模型的软件实现,以进行安全性的实验验证。

著录项

  • 作者

    Banerjee, Ayan.;

  • 作者单位

    Arizona State University.;

  • 授予单位 Arizona State University.;
  • 学科 Health Sciences Health Care Management.;Computer Science.
  • 学位 Ph.D.
  • 年度 2012
  • 页码 239 p.
  • 总页数 239
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号