-
内容大纲
反应式和并发系统指实时运行的计算系统,如操作系统、控制系统、交互系统和并发系统。这些系统很难规约、实现和验证,主要原因是系统与其环境之间及系统本身的并行进程之间交互的复杂性,在交互时间上的微小变化可能导致完全不同的行为。
时序逻辑是一种形式化规约语言,可用于刻画和分析反应式系统中有关时间和行为方面的属性。它提供了一种简单、自然但精确的方式来讨论交互发生的顺序,而无须采用绝对时间度量。本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型。
本书是国际著名计算机科学家Zohar Manna和Amir Pnueli(图灵奖得主)的代表作,适合作为计算机、软件工程、人工智能、自动化等专业高年级本科生、研究生的教材或参考书,也可供相关领域的研究人员和技术开发人员参考。 -
作者介绍
-
目录
第Ⅰ部分 并发模型
第1章 基本模型
1.1 通用模型
1.1.1 基础语言
1.1.2 基本转换系统
1.1.3 转换关系pι
1.1.4 使能与非使能转换
1.1.5 空转换与勤勉转换
1.1.6 计算
1.1.7 具体模型
1.2 模型1:转换图
1.2.1 声明
1.2.2 进程
1.2.3 基本转换系统图
1.2.4 用交错表示并发性
1.2.5 调度
1.3 模型2:共享变量文本
1.3.1 简单语句
1.3.2 复合语句
1.3.3 程序
1.3.4 文本程序中的标记
1.3.5 标记等价关系
1.3.6 文本语言中的位置
1.4 共享变量文本语义
1.4.1 状态变量和状态
1.4.2 转换
1.4.3 初始条件
1.4.4 计算
1.4.5 下标变量
1.5 语句间的结构关系
1.5.1 子语句
1.5.2 控制谓词at、after和in
1.5.3 语句的使能性
1.5.4 进程和并行语句
1.5.5 竞争语句
1.6 行为等价
1.6.1 初步近似
1.6.2 可观测和可简化的行为
1.6.3 转换系统的等价性
1.6.4 语句一致性
1.6.5 例子
1.6.6 模拟与实现
1.7 分组语句
1.7.1 分组语句
1.7.2 与分组语句关联的转换
1.8 信号量语句
1.8.1 信号量需求
1.8.2 信号量语句
1.8.3 互斥信号量的应用
1.8.4 信号量的其他应用
1.9 区域语句
1.9.1 比较信号量和区城语句
1.9.2 选择语句中的同步
1.10 模型3:消息传递文本
1.10.1 通信语句
1.10.2 缓冲能力
1.10.3 例子
1.10.4 条件通信语句
1.10.5 同步模型和异步模型的比较
1.10.6 公平服务器
1.11 模型4:Petri网
1.11.1 网
1.11.2 标记
1.11.3 图形化表示
1.11.4 点火
1.11.5 Petri系统
1.11.6 例子
问题
文献注释
第2章 真并发模型
2.1 交错和并发
2.1.1 重叠执行
2.1.2 交错计算
2.1.3 细粒度
2.2 限制临界引用
……
第Ⅱ部分 规约
参考文献
同类热销排行榜
- C语言与程序设计教程(高等学校计算机类十二五规划教材)16
- 电机与拖动基础(教育部高等学校自动化专业教学指导分委员会规划工程应用型自动化专业系列教材)13.48
- 传感器与检测技术(第2版高职高专电子信息类系列教材)13.6
- ASP.NET项目开发实战(高职高专计算机项目任务驱动模式教材)15.2
- Access数据库实用教程(第2版十二五职业教育国家规划教材)14.72
- 信号与系统(第3版下普通高等教育九五国家级重点教材)15.08
- 电气控制与PLC(普通高等教育十二五电气信息类规划教材)17.2
- 数字电子技术基础(第2版)17.36
- VB程序设计及应用(第3版十二五职业教育国家规划教材)14.32
- Java Web从入门到精通(附光盘)/软件开发视频大讲堂27.92
推荐书目
-
孩子你慢慢来/人生三书 华人世界率性犀利的一枝笔,龙应台独家授权《孩子你慢慢来》20周年经典新版。她的《...
-
时间简史(插图版) 相对论、黑洞、弯曲空间……这些词给我们的感觉是艰深、晦涩、难以理解而且与我们的...
-
本质(精) 改革开放40年,恰如一部四部曲的年代大戏。技术突变、产品迭代、产业升级、资本对接...