导语

  

内容提要

  

    拉吉夫·阿卢尔编著的《信息物理融合系统原理》主要介绍信息物理融合系统的基本理论，包括系统设计、规约、建模和分析方法。针对基于模型的设计、并发理论、分布式算法、形式化的规约和验证方法、控制理论、实时系统和混成系统等分支学科。从不同侧面对信息物理融合系统进行描述。本书采用数学化的建模、规约与分析等概念，并配以案例阐述信息物理系统所涉及的分布式算法、网络协议、控制设计和机器人等理论。
    本书适合作为计算科学、计算机工程和电子工程相关学科的高年级本科生或一年级研究生的教材。

    拉吉夫·阿卢尔(Rajeev Alur)，现为宾夕法尼亚大学计算机和信息科学Zisman Family教授，该校嵌入式系统硕士生课程主管。他于1991年获得斯坦福大学计算机科学博士学位，在1997年加入宾夕法尼亚大学之前，在贝尔实验室计算机科学研究中心工作。他的研究方向涉及计算机的3个子学科：理论计算机科学系统、系统设计的形式化方法、信息物理融合系统。他是ACM Fellow和DIEEE Fellow；并曾担任ACM SIGBED主席LICS大会主席。

出版者的话
译者序
前言
第1章 简介
  1.1 什么是信息物理融合系统
  1.2 信息物理融合系统的主要特征
  1.3 研究主题概述
  1.4 课程组织指南
第2章 同步模型
  2.1 反应式构件
    2.1.1 变量、值和表达式
    2.1.2 输入、输出和状态
    2.1.3 初始化
    2.1.4 更新
    2.1.5 执行
    2.1.6 扩展状态机
  2.2 构件属性
    2.2.1 有限状态构件
    2.2.2 复合构件
    2.2.3 事件触发构件
    2.2.4 非确定性构件
    2.2.5 输入使能构件
    2.2.6 任务图和等待依赖关系
  2.3 构件构成
    2.3.1 方框图
    2.3.2 输入/输出变量重命名
    2.3.3 并行组合
    2.3.4 输出隐藏
  2.4 同步设计
    2.4.1 同步电路
    2.4.2 巡航控制系统
    2.4.3 同步网络
  参考文献说明
第3章 安全性需求
  3.1 安全性规约
    3.1.1 迁移系统的不变量
    3.1.2 需求在系统设计中的作用
    3.1.3 安全监控器
  3.2 验证不变量
    3.2.1 证明不变量
    3.2.2 不变量的自动验证
    3.2.3 基于模拟的分析
  3.3 枚举搜索
  3.4 符号搜索
    3.4.1 符号迁移系统
    3.4.2 符号广度优先搜索
    3.4.3 约简有序二叉判定图
  参考文献说明
第4章 异步模型
  4.1 异步进程
    4.1.1 状态、输入和输出
    4.1.2 输入、输出和内部动作
    4.1.3 执行
    4.1.4 扩展的状态机
    4.1.5 进程操作
    4.1.6 安全性需求
  4.2 异步设计原语
    4.2.1 阻塞同步与非阻塞同步
    4.2.2 死锁
    4.2.3 共享存储器
    4.2.4 公平性假设
  4.3 异步协调协议
    4.3.1 领导选举
    4.3.2 可靠传输
    4.3.3 等待无关共识
  参考文献说明
第5章 活性需求
  5.1 时序逻辑
    5.1.1 线性时序逻辑
    5.1.2 LTL规约
    5.1.3 异步进程的LTL规约
    5.1.4 超越
  5.2 模型检查
    5.2.1 Büchi自动机
    5.2.2 从LTL到Büchi自动机
    5.2.3 嵌套深度优先搜索
    5.2.4 符号重复性检查
  5.3 活性证明
    5.3.1 eventuality属性
    5.3.2 条件response属性
  参考文献说明
第6章 动态系统
  6.1 连续时间模型
    6.1.1 连续变化的输入和输出
    6.1.2 扰动模型
    6.1.3 构件构成
    6.1.4 稳定性
  6.2 线性系统
    6.2.1 线性度
    6.2.2 线性微分方程的解
    6.2.3 稳定性
  6.3 控制器设计
    6.3.1 开环控制器与反馈控制器
    6.3.2 稳定化控制器
    6.3.3 PID控制器
  6.4 分析技术
    6.4.1 数值模拟
    6.4.2 栅栏函数
  参考文献说明
第7章 时间模型
  7.1 时间进程
    7.1.1 基于时间的电灯开关
    7.1.2 有界延迟的缓冲器
    7.1.3 多个时钟
    7.1.4 形式化模型
    7.1.5 时间进程组合
    7.1.6 不完全时钟的建模
  7.2 基于时间的协议
    7.2.1 基于时间的分布式协调
    7.2.2 音频控制协议
    7.2.3 双腔植入式心脏起搏器
  7.3 时间自动机
    7.3.1 时间自动机的模型
    7.3.2 区域等价
    7.3.3 基于矩阵表示的符号分析
  参考文献说明
第8章 实时调度
  8.1 调度概念
    8.1.1 调度器架构
    8.1.2 周期作业模型
    8.1.3 可调度性
    8.1.4 其他的作业模型
  8.2 EDF调度
    8.2.1 周期作业模型的
    8.2.2 EDF的最优性
    8.2.3 基于利用率的可调度性测试
  8.3 固定优先级调度
    8.3.1 单调截止期策略和单调速率策略
    8.3.2 单调截止期策略的最优性
    8.3.3 单调速率策略的可调度性测试
  参考文献说明
第9章 混成系统
  9.1 混成动态模型
    9.1.1 混成进程
    9.1.2 进程组合
    9.1.3 奇诺行为
    9.1.4 稳定性
  9.2 混成系统设计
    9.2.1 自动驾驶车辆
    9.2.2 多机器人协调的障碍规避
    9.2.3 多跳控制网络
  9.3 线性混成自动机
    9.3.1 追赶游戏例子
    9.3.2 形式化模型
    9.3.3 符号可达性分析
  参考文献说明
参考文献
索引