• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Formal specification and verification of reconfigurable hybrid systems.
【24h】

Formal specification and verification of reconfigurable hybrid systems.

机译：可重构混合系统的正式规范和验证。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

A reconfigurable hybrid system is a collection of digital and analog components, where digital components are embedded in and interact with analog components and their configuration can be changed by means of physical or logical mobility of components. To establish a formal framework for the specification and verification of such systems, we extend the pi-calculus, a process algebraic formalism for mobile concurrent computation, to hybrid setting. The outcome is the &phis;-calculus, whose main features in syntactic extensions are information hiding of analog variables, dynamic instantiations and mobility of analog components. The structural operational semantics of the &phis;-calculus is defined with a set of transition rules. We show a certain congruence of hybrid processes under defined bisimulation in arbitrary analog environment. Another direction for the verification is pursued by specifying requirements in linear-time temporal logic and checking whether the system model satisfies the requirement logic formula. The well-known software model checker SPIN is found to be very suitable for the verification of reconfigurable systems. A hybrid extension to SPIN is implemented using an efficient geometric processing library. We show that the resulting model checker SPHIN is capable of verifying important requirements of interesting reconfigurable hybrid systems such as models of assembly factory robots and flocking agents.
机译：可重新配置的混合系统是数字和模拟组件的集合，其中数字组件被嵌入模拟组件并与之交互，并且可以通过组件的物理或逻辑移动性来更改其配置。为了建立用于规范和验证此类系统的正式框架，我们将pi-演算（一种用于移动并发计算的过程代数形式主义）扩展到混合设置。结果就是φ微积分，其语法扩展的主要特征是模拟变量的信息隐藏，动态实例化和模拟组件的移动性。演算的结构操作语义是通过一组转换规则定义的。我们在任意模拟环境中的定义双仿真下显示了混合过程的一定一致性。通过在线性时间时序逻辑中指定需求并检查系统模型是否满足需求逻辑公式，从而寻求验证的另一个方向。发现著名的软件模型检查器SPIN非常适合验证可重新配置的系统。使用高效的几何处理库可实现SPIN的混合扩展。我们证明，结果模型检查器SPHIN能够验证有趣的可重构混合系统的重要要求，例如组装工厂机器人和植绒代理的模型。

著录项

  • 作者

    Song, Hosung.;

  • 作者单位

    University of Michigan.;

  • 授予单位 University of Michigan.;
  • 学科 Computer Science.
  • 学位 Ph.D.
  • 年度 2005
  • 页码 147 p.
  • 总页数 147
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 自动化技术、计算机技术;
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号