嵌入式系统导论:CPS方法
作者 : (美)Edward Ashford Lee, Sanjit Arunkumar Seshia 著
译者 : 李实英 贺蓉 李仁发 译
丛书名 : 计算机科学丛书
出版日期 : 2011-12-07
ISBN : 978-7-111-36021-6
定价 : 55.00元
教辅资源下载
扩展信息
语种 : 简体中文
页数 : 269
开本 : 16
原书名 : Introduction to Embedded Systems - A Cyber-Physical Systems Approach
原出版社: Edward Ashford Lee, Sanjit Arunkumar Seshia
属性分类: 教材
包含CD :
绝版 :
图书简介

不同于大多数嵌入式系统的书籍着重于计算机技术在嵌入式系统中的应用,本书的重点则是论述系统模型与系统实现的关系,以及软件和硬件与物理环境的相互作用。本书是业界第一本关于CPS(信息物理系统)的专著。CPS 将计算、网络和物理过程集成在一起,CPS的建模、设计和分析成为本书的重点。
  从CPS的视角,围绕系统的建模、设计和分析这三个方面,本书分成四个大部分。建模部分包括第2章到第6章,分别讲述动态建模、离散建模和混合建模,以及状态机的并发组合与并发计算模型。设计部分强调嵌入式系统中处理器,存储结构,输入输出,多任务处理和实时调度的算法与设计,以及这些设计在CPS中的主要作用。分析部分着重于对系统特性进行精确描述、规范比较和规范与产品设计的分析方法以及嵌入式软件特性的定量分析方法。第四部分包括连个附录,提供了一些数学和计算机科学的背景知识,有助于加深对文中给出知识的理解。

  这本书的教辅资料暂时没有,需要上网在线注册,或是与作者联系索取,作者邮箱:authors@leeseshia.com;网上链接:http://chess.eecs.berkeley.edu/instructors/,网上注册:https://chess.eecs.berkeley.edu/login/?subpage=Request&group=instructors。

图书特色

嵌入式系统导论
CPS方法
Introduction to Embedded Systems A Cyber-Physical Systems Approach 
(美)Edward Ashford Lee 加州大学伯克利分校  Sanjit Arunkumar Seshia 加州大学伯克利分校 著 李实英 贺蓉 李仁发 译
本书是一本关于CPS (Cyber-Physical System,信息物理系统)的著作。不同于大多数嵌入式系统的书籍着重于计算机技术在嵌入式系统中的应用,本书的重点是论述系统模型与系统实现的关系,以及软件和硬件与物理环境的相互作用。
全书从CPS的视角,围绕系统的建模、设计和分析三方面,深入浅出地介绍了设计和实现CPS的整体过程及各个阶段的细节。建模部分介绍如何模拟物理系统,主要关注动态行为模型,包括动态建模、离散建模和混合建模,以及状态机的并发组合与并行计算模型。设计部分强调嵌入式系统中处理器、存储器架构、输入和输出、多任务处理和实时调度的算法与设计,以及这些设计在CPS中的主要作用。分析部分重点介绍一些系统特性的精确规格、规格之间的比较方法、规格与产品设计的分析方法以及嵌入式软件特性的定量分析方法。此外,两个附录提供了一些数学和计算机科学的背景知识,有助于加深读者对文中所给知识的理解。

作者简介
Edward Ashford Lee 拥有加州大学伯克利分校博士学位,曾为加州大学伯克利分校电子工程与计算机科学系主任,现为该系Robert S. Pepper特聘教授。他的主要研究方向是嵌入式与实时计算系统的设计、建模和模拟。Lee教授是IEEE会员,于1997年获得工程教育领域的Frederick Emmons Terman奖。
Sanjit Arunkumar Seshia 拥有卡内基-梅隆大学计算机科学专业博士学位,现为美国加州大学伯克利分校电子工程与计算机科学系副教授。他的主要研究方向是可信计算和计算逻辑。他获得了科学和工程领域的总统早期职业生涯奖(PECASE)和Alfred P. Sloan研究奖金。

图书前言

关于此书
  计算机和软件最显著的用途是处理人们所使用的信息。我们用计算机和软件写教材(如本书)、在网上搜索信息、通过电子邮件进行通信以及跟踪财务数据。然而,绝大多数应用中的计算机并非如此显而易见。这些计算机运行于汽车上的引擎、刹车、安全带、安全气囊和音响系统中。它们将声音进行数字编码并转换成无线电信号,然后从手机发送到基站。它们控制微波炉、冰箱和洗碗机。它们运行各种打印机,从台式喷墨打印机到大型工业用的高容量打印机。它们指挥车间里的机器人、发电厂的电力生产、化工厂的各种工序,以及城市的交通灯。它们在生物样本中搜寻细菌,构建人体内部图像,以及测量生命体征。它们处理来自太空的无线电信号,寻找超新星和外星智慧生物。它们给人类生活带来各种玩具,而且让这些玩具能对人的触摸和声音有所反应。它们控制飞机和火车。这些不显眼的计算机称为嵌入式系统(embedded system),而在嵌入式系统上运行的软件称为嵌入式软件(embedded software)。
  尽管嵌入式系统得到如此广泛的应用,但是从计算机科学相对短暂的发展历史来看,它主要致力于信息处理。直到最近,嵌入式系统才受到研究人员的更多关注。研究界认识到,设计和分析嵌入式系统所需的工程技术是与通用计算机系统不同的。尽管嵌入式系统从20世纪70年代就开始应用,但是长期以来,这些系统被简单地视做小型计算机。最主要的工程问题被理解为如何运用有限资源(有限的处理能力、有限的电源、小型存储器等)的问题。这样一来,工程挑战成为优化设计。由于所有设计都得益于优化,所以该学科与计算机科学的其他方面相比并没有什么独特的地方。它只在应用同样的优化方法方面必须更加积极投入。
  目前,研究界已经认识到,嵌入式系统中最主要的挑战来自于它们与物理过程的相互作用,而不是它们的有限资源。“CyberPhysical System”(CPS)这个术语由美国国家科学基金会的Helen Gill提出,用于描述计算与物理过程的整合。在CPS中,嵌入式的计算机和网络通常采用反馈回路来监视和控制物理过程,在反馈回路中物理过程和计算相互影响。因而,这种系统设计需要理解计算机、软件、网络和物理过程的动态融合。正是对于动态融合(joint dynamics)的研究将这个学科与其他学科分离开来。
  在研究CPS的过程中,会遇到一些在通用计算中很少出现的关键问题。例如,在通用软件中,执行一个任务的时间与性能相关,但不与正确性相关。执行一个任务耗费更长时间并不是不正确的,只是不太方便,因而不那么有价值。但是在CPS中,执行一个任务所需的时间可能对系统的正确功能实现至关重要。与信息世界相反,在物理世界中时间的流逝是必然的。
  而且,在CPS中许多事情会同时发生。物理过程是许多同时发生事情的组合,这与深深植根于顺序步骤中的软件进程不同。Abelson and Sussman(1996)将计算机科学描述为“程序化认识论”(procedural epistemology),即知识贯穿于整个程序。相对而言,在物理世界中,过程很少是程序化的。物理过程是许多并行过程的组合。通过调和影响这些过程的行为来对这些过程的动态状况进行测量和控制是嵌入式系统的主要任务。因此,并发性是CPS固有的。在设计和分析嵌入式软件时,许多技术挑战源于必须建立原本顺序的语义与本质上并发的物理世界之间的桥梁。
写作目的
  当今,使计算机与物理过程协作需要复杂的技术和底层的设计。因此嵌入式软件设计人员不得不与中断控制器、存储器架构、汇编级编程(以开发专用指令或进行精确的时间控制)、设备驱动程序设计、网络接口和调度策略打交道,而不是只关注所要实现的行为。这些技术的高质量和复杂性需要我们重点掌握一些入门知识。这些知识着重于如何对软件、网络和物理过程的动态融合进行建模和设计,介绍实现这些动态融合的最新(而不是过去的)方法。本书正是力求成为这样一本教材。
  大多数关于嵌入式系统的书籍侧重于使计算机与物理系统交互所需的技术(Barr and Massa, 2006; Berger, 2002; Burns and Wellings, 2001; Kamal, 2008; Noergaard, 2005; Parab et al, 2007; Simon, 2006; Valvano, 2007;Wolf, 2000)。其他书籍则着重于将计算机技术(如编程语言、操作系统、网络等)应用于嵌入式系统中的技术问题(Buttazzo, 2005a; Edwards, 2000; Pottie and Kaiser, 2005)。虽然这些实现技术可以满足设计人员使嵌入式系统正常工作的需求,但并不是构成该学科的智能核心。其智能核心是将计算与物理动态结合在一起的模型和抽象化。
  有些教科书在该方向上付出了很多努力。 Jantsch (2003)着重于并发计算模型,Marwedel(2003)侧重于软件和硬件的行为模式,Sriram and Bhattacharyya (2009)关注信号处理行为的数据流模型及其在可编程DSP上的映射。以上都是非常良好的开端。并发模型(如数据流)以及软件的抽象模型(如状态图)可以作为比命令式编程语言(如C)、中断和线程以及设计人员必须解决的架构问题(比如缓存)更好的开端。然而,这些教材并不适合入门课程。它们要么太专业要么太高级,或者两者兼而有之。本书力求成为一本入门式的教材,侧重于介绍系统模型及其与系统实现之间的关系。
  本书的主题是关于系统模型以及它们与系统实现的关系。这些模型主要是动态的,即系统状态随时间演化。我们不介绍关于组成系统静态信息的结构模型,尽管这些模型对于嵌入式系统设计也非常重要。
  应用模型有一个很大的优势。模型具有形式上的特性。可以利用模型定义事件。例如,可以断言一个模型是确定性的(deterministic),也就是说,给定相同的输入,它总是产生相同的输出。系统的任何物理实现都不能进行这样绝对的断言。如果模型是对一个物理系统的良好抽象(在此,“良好抽象”是指它只忽略了一些无关紧要的细节),那么模型的决定性断言可以增加系统物理实现的可靠性。这种可靠性是极具价值的,尤其对于嵌入式系统而言,其出现的故障可能危及人的生命。通过学习系统模型可以了解这些系统在物理世界中是如何运行的。
  我们的重点是软件和硬件与所处物理环境的相互作用。这就要求对软件和网络的时序动态进行明确建模并精确描述应用中固有的并发特性。事实上,实现技术还不能满足这一要求,这当然不能成为我们传授错误的工程方法的理由,而应该按照设计和建模应该有的形式进行教学,并以如何通过最新技术(部分)实现这些目标的关键表述来丰富其内容。因此,当今的嵌入式系统技术,不应该如上述许多教材那样,被描述成一大堆事实和技巧,而应该脚踏实地逐步实现合理的设计实践,重点应该放在什么是合理的设计实践,以及如今的技术如何阻碍和实现它。
  Stankovic et al(2005)支持这一观点,指出“现有的RTES(实时嵌入式系统)设计技术并不能有效地支持可靠而鲁棒的嵌入式系统开发”。他们提出需要“提高编程抽象化的水平”。我们认为,只提高抽象化水平是不够的,应该从根本上改变所使用的抽象。例如,如果没有建立于其上的底层抽象,软件的时间特性则不能有效地利用更高层次的抽象。
  我们需要采用鲁棒性好、可预见且具有可重复时序动态的设计(Lee,2009a),这必须通过建立能适当反映信息物理系统实际情况的抽象来实现。其结果将使CPS的设计更加复杂,包括更多的自适应控制逻辑、时间演化,以及安全性和可靠性的提高,而避免当今设计的不稳定,很小的改变都成为大问题。
除了处理时序动态,CPS设计总是面临并发问题的挑战。由于软件是植根于顺序抽象,并发机制(如中断和多任务处理,利用信号和互斥锁)变得非常重要。因此,我们在本书中特别强调对线程、消息传递、死锁避免、竞争条件和数据决策等关键内容的理解。
本书未尽事宜
  本书的版本并不完整。实际上,要完全涵盖CPS意义上的嵌入式系统是不可能的。其中涵盖了Berkeley(伯克利)本科嵌入式系统课程(http://LeeSeshiaorg)的具体内容,并希望在将来的版本中包括:传感器和制动器、网络、容错、安全性、仿真技术、控制系统以及硬件/软件协同设计。
如何使用本书
  本书分为三个主要部分,分别关注建模、设计和分析,如图1所示。这三个部分彼此相对独立,在很大程度上是为了能同时学习。利用虚线框出的七个分区可以实现系统性的学习。每个分区包括两章,假设每个分区需要花两周时间,并且绪论和结束部分各花一周时间,则本书可以在15周内学完。

图1本书各章节之间依赖性强弱分布图。黑色箭头表示章节之间有强依赖关系,灰色箭头表示章节之间有弱依赖关系。如果章节i和章节j之间有弱依赖关系,则可以只学习章节j,而不学习章节i,或者略去一些实例或具体的分析方法
  附录提供的背景资料在其他教材中也很详尽,但是收入本书对学习可以提供很大帮助。附录A介绍的是集合和函数的概念,这些概念可以提高嵌入式系统学习中常见的精确度。附录B介绍的是复杂度和可计算性理论的基本成果,这些可以加深理解系统建模和分析中的问题。值得注意的是,附录B依赖于第3章讲述的状态机理论,因此应该在读完第3章之后进行学习。
  由于技术的最新发展从根本上改变了出版业的技术,本书英文原版以非传统方式出版。至少当前的版本可以以PDF文件方式在线阅读,可从网站http://LeeSeshiaorg上免费获取。布局适合于中型屏幕,尤其是笔记本电脑、iPad以及其他平板电脑。此外,大量使用超链接和色彩以加强在线阅读体验。
  我们力图使英文书适用于电子书形式,理论上可以在不同大小的屏幕上阅读,从而充分利用现有的显示屏。然而,类似于HTML文档,电子书的格式采用回流技术,使页面布局即时重新绘制。其结果非常依赖于屏幕的大小,在很多屏幕上显得有些怪异,不是最优的显示。因此,我们选择性地对布局进行了控制,不建议在iPhone上阅读。
读者对象
  本书适用于高年级本科生或低年级研究生,以及想要了解嵌入式系统工程原理的实践工程师和计算机专家。读者需要懂得计算机结构(如知道什么是ALU)、计算机编程(本书采用C语言)、基本的离散数学和算法知识,最好对信号和系统也有所了解(比如何为对连续信号进行采样)。
致谢
  感谢以下人员在过去三年中对本书的贡献和提出的宝贵建议:Murat Arcak, Janette Cardoso, Gage Eads, Stephen Edwards, Suhaib Fahmy, ShannaShaye Forbes, Jeff C Jensen, Jonathan Kotker, Wenchao Li, Isaac Liu, Slobodan Matic, Le Ngoc Minh, Steve Neuendorffer, Minxue Pan, Hiren Patel, Jan Reineke, Rhonda Righter, Chris Shaver, Stavros Tripakis, Pravin Varaiya, Maarten Wiggers, Qi Zhu, 以及UC Berkeley的EECS 149班的学生,尤其是Ned Bass 和Dan Lynch。特别感谢Elaine Cheong认真审阅了大多数章节并提出了有益的建议。特别感谢家人的忍耐和支持,尤其是Helen、Katalina、Rhonda (来自 Edward), 以及Appa、Amma、Ashwin和 Bharathi (来自Sanjit)。
错误反馈
  如果发现本书中的错误或印刷错误,或者如果有改进或其他建议,请发送电子邮件到authors@leeseshiaorg。
  请注明该书的版本号和相关的页码,无论是电子版或纸质版。非常感谢!
扩展阅读
  最近几年出现了很多嵌入式系统方面的教材。这些教材以各种不同的方式介绍这一主题,往往反映一些与嵌入式系统紧密结合的成熟领域的发展前景,如VLSI设计、控制系统、信号处理、机器人、实时系统或软件工程。其中有些教材可以作为本书的有益补充,强烈推荐给那些想要深入理解嵌入式系统的读者。
  具体而言,Patterson and Hennessy (1996)尽管不是以嵌入式处理器作为重点,但它是一本计算机架构的经典教材,是对嵌入式处理器架构感兴趣的读者必读的。Sriram and Bhattacharyya (2009)侧重于信号处理应用,如无线通信和数字媒体,并全面介绍了数据流编程方法。Wolf (2000)对硬件设计技术和微处理器架构以及它们对嵌入式软件设计的影响给出了精彩的概述。Mishra and Dutt (2005) 介绍了基于结构描述语言(ADL)的嵌入式架构。Oshana (2006) 专门介绍了Texas Instruments(德州仪器)公司(TI)的DSP处理器,综述了架构方法和汇编级编程。
  在软件上,Buttazzo(2005a)对实时软件的调度技术进行了全面综述。Liu (2000)对处理软件中的突发实时事件提供了一个目前为止最好的方法。Edwards (2000)介绍了一种用于嵌入式系统设计的域专用高级编程语言。Pottie and Kaiser (2005) 综合介绍了网络技术,特别是嵌入式系统中的无线技术。Koopman (2010)侧重于嵌入式软件的设计过程,包括需求管理、项目管理、测试计划和安全计划。
  没有任何一本教材可以全面涵盖所有技术,提供给嵌入式系统工程师。很多教材提供了关于当前设计技术的有益信息(Barr and Massa, 2006; Berger, 2002; Burns and Wellings, 2001; Gajski et al, 2009; Kamal, 2008;Noergaard, 2005; Parab et al, 2007; Simon, 2006)。
致教师
  在Berkeley,本书用于高年级本科生课程“嵌入式系统导论”。通过本书的网站主页http://LeeSeshiaorg可以获得大量讲座和实验的资料。另外,还可以获得解题手册。请联系authors@leeseshiaorg。

上架指导

计算机科学及应用

封底文字

本书是一本关于CPS (Cyber-Physical System,信息物理系统)的著作。不同于大多数嵌入式系统的书籍着重于计算机技术在嵌入式系统中的应用,本书的重点是论述系统模型与系统实现的关系,以及软件和硬件与物理环境的相互作用。
全书从CPS的视角,围绕系统的建模、设计和分析三方面,深入浅出地介绍了设计和实现CPS的整体过程及各个阶段的细节。建模部分介绍如何模拟物理系统,主要关注动态行为模型,包括动态建模、离散建模和混合建模,以及状态机的并发组合与并行计算模型。设计部分强调嵌入式系统中处理器、存储器架构、输入和输出、多任务处理和实时调度的算法与设计,以及这些设计在CPS中的主要作用。分析部分重点介绍一些系统特性的精确规格、规格之间的比较方法、规格与产品设计的分析方法以及嵌入式软件特性的定量分析方法。此外,两个附录提供了一些数学和计算机科学的背景知识,有助于加深读者对文中所给知识的理解。

作者简介

(美)Edward Ashford Lee, Sanjit Arunkumar Seshia 著:Edward Ashford Lee 拥有加州大学伯克利分校博士学位,曾为加州大学伯克利分校电子工程与计算机科学系主任,现为该系Robert S. Pepper特聘教授。他的主要研究方向是嵌入式与实时计算系统的设计、建模和模拟。Lee教授是IEEE会员,于1997年获得工程教育领域的Frederick Emmons Terman奖。 Sanjit Arunkumar Seshia 拥有卡内基-梅隆大学计算机科学专业博士学位,现为美国加州大学伯克利分校电子工程与计算机科学系副教授。他的主要研究方向是可信计算和计算逻辑。他获得了科学和工程领域的总统早期职业生涯奖(PECASE)和Alfred P. Sloan研究奖金。

译者简介

李实英 贺蓉 李仁发 译:暂无简介

译者序

不同于大多数嵌入式系统的书籍着重于计算机技术在嵌入式系统中的应用,本书的重点是论述系统模型与系统实现的关系,以及软件和硬件与物理环境的相互作用。本书是业界第一本关于CPS(CyberPhysical System,信息物理系统)的专著。
  原书作者美国加州大学伯克利分校Edward Ashford Lee教授是世界上嵌入式系统领域的著名学者,也是CPS研究的倡导者和引领者之一。Lee教授领导的团队还开发了一个叫做Ptolemy Ⅱ的系统,这是一个非常优秀的开源嵌入式系统研究与开发平台,可惜国内了解的人不多。
  CPS将计算、网络和物理过程集成在一起,CPS的建模、设计和分析成为本书的重点。
  从CPS的视角,围绕系统的建模、设计和分析这三个方面,本书分成四大部分。第一部分包括第2~6章,分别讲述动态建模、离散建模和混合建模,以及状态机的并发组合与并发计算模型。第二部分包括第7~11章,强调嵌入式系统中处理器、存储器架构、输入和输出、多任务处理和实时调度的算法与设计,以及这些设计在CPS中的主要作用。第三部分包括第12~15章,重点介绍一些系统特性的精确规格、规格之间的比较方法、规格与产品设计的分析方法以及嵌入式软件特性的定量分析方法。第四部分包括两个附录,提供了一些数学和计算机科学的背景知识,有助于加深对文中所介绍知识的理解(可以登录网站http://LeeSeshiaorg获取本书的英文版和更多信息)。
  李仁发教授负责本书的整体翻译工作。李实英博士主译了前言、第1章以及第一部分和第二部分,贺蓉博士主译了第三部分和第四部分。此外,参与本书翻译工作的还有谢勇、黄鑫、杜家宜、王震、高楠、宋倩、刘琳、周权、吴武飞、谷连军、何翔、许文龙、吴文康、黄晶、李志灿和胡环。
  把一种语言表达转换成另一种是一件困难的事情。看似很直白的一个词,虽然理解其词义,但要换一种语言表达时往往煞费苦心,况且CPS的研究在国内尚处于起步阶段,许多名词还很难给出确切的中文译名。译者力求忠实地表达书中所介绍的技术,保持原作者的行文风格。此外,本书的翻译以Leesheshia_DigitalV1_03为基础,并根据作者更新的版本(Leesheshia_DigitalV1_05)进行了校对,修正了原稿中的一些改动。限于时间(急于想把此书介绍给国内读者)以及译者水平和经验的不足,译文中难免存在许多不当之处,恳请读者提出宝贵的意见。
  本书在翻译过程中得到了Edward Ashford Lee教授本人的直接帮助,同时还得到湖南大学嵌入式系统与网络实验室同仁及机械工业出版社许多人士的帮助。对此,译者深表感谢。

图书目录

出版者的话
译者序
前言
符号
第1章绪论
11应用
12一个实例
13设计过程
131建模
132设计
133分析
14小结
第一部分动态行为建模
第2章连续动态
21牛顿力学
22参量模型
23系统的特性
231因果关系系统
232无记忆系统
233线性和时不变性
234稳定性
24反馈控制
25小结
练习
第3章离散动态
31离散系统
32状态的概念
33有限状态机
331转移
332发生响应时
333升级函数
334确定性和可接受性
34扩展状态机
35非确定性
351形式化模型
352非确定性的用途
36行为和轨迹
37小结
练习
第4章混合系统
41模态模型
411状态机的参量模型
412连续输入
413状态精化
42混合系统的分类
421时间自动机
422高阶动态
423管理控制
43小结
练习
第5章状态机的组合
51并发组合
511并列同步组合
512并列异步组合
513共享变量
514级联组合
515通用组合
52分层状态机
53小结
练习
第6章并发计算模型
61模型结构
62同步响应模型
621反馈模型
622形式规范和形式不规范模型
623构建一个固定点
63数据流计算模型
631数据流原理
632同步数据流
633动态数据流
634结构化数据流
635进程网络
64实时计算模型
641时间触发模型
642离散事件系统
643连续时间系统
65小结
练习
第二部分嵌入式系统设计
第7章嵌入式处理器
71处理器类型
711微控制器
712DSP处理器
713图形处理器
72并行处理
721并行处理与并发处理
722流水线
723指令级并行
724多核架构
73小结
练习
第8章存储器架构
81存储技术
811RAM
812非易失性存储器
82存储器层次结构
821存储映射
822寄存器文件
823便签式存储器和高速缓冲存储器
83存储模型
831存储地址
832栈
833存储器保护单元
834动态存储分配
835C的存储模型
84小结
练习
第9章输入和输出
91I/O硬件
911脉宽调制
912通用数字I/O
913串行接口
914并行接口
915总线
92并发环境下的顺序软件
921中断和异常
922原子性
923中断控制器
924中断建模
93模拟/数字接口
931数模转换和模数转换
932信号调节
933采样和走样
94小结
练习
第10章多任务处理
101命令式程序
102多线程
1021创建线程
1022实现多线程
1023互斥
1024死锁
1025存储一致性模型
1026多线程问题
103进程和消息传递
104小结
练习
第11章调度
111调度的基础知识
1111调度决策
1112任务模型
1113调度程序的比较
1114调度程序的实现
112单调速率调度
113最早时限优先
114调度和互斥
1141优先级倒置
1142优先级继承协议
1143优先级上限协议
115多处理器调度
116小结
练习
第三部分分析和验证
第12章不变量与时序逻辑
121不变量
122线性时序逻辑
1221命题逻辑公式
1222LTL公式
1223LTL公式的应用
123小结
练习
第13章等价与精化
131规格建模
132类型等价与类型精化
133语言等价与包含
134模拟
1341模拟关系
1342形式化模型
1343传递性
1344模拟关系的非唯一性
1345模拟与语言包含
135互模拟
136小结
练习
第14章可到达性分析和模型检测
141开放式与封闭式系统
142可到达性分析
1421Gp验证
1422显态模型检测
1423符号化模型检测
143模型检测中的抽象
144活跃属性的模型检测
1441属性的自动机表达
1442寻找可接受循环
145小结
练习
第15章定量分析
151关注的问题
1511极限分析
1512阈值分析
1513一般情况分析
152程序图
1521基本块
1522控制流图
1523函数调用
153执行时间的决定因素
1531循环界限
1532指数的路径空间
1533路径的可行性
1534存储层次
154执行时间分析的基础
1541最优化问题的形式化
1542逻辑流约束
1543基本块的界限
155其他定量分析问题
1551存储界限分析
1552能耗和功耗分析
156小结
练习
第四部分附录
附录A集合和函数
附录B复杂度和可计算性理论
参考书目

教学资源推荐
作者: [美]威廉·斯托林斯(William Stallings)著
作者: 袁春风,朱光辉,余子濠
参考读物推荐
作者: (美)Elecia White 著