形式化方法Formal Methods (实例研究)裘宗燕北京大学数学学院2006年2－6月2006年4月2实例1：实时内核问题简介 实时内核进程状态和内核数据结构（原文档） 内核状态后台处理 中断处理 总结2006年4月3简介•嵌入式系统得到越来越广泛的应用•需要一个小操作系统提供进程调度和中断处理功能•嵌入式系统应用有时是安全攸关和生命攸关的•下面的研究是用Z 描述了一个X 光治疗仪的内核•原系统包含大约50 页汇编代码，生成的目标代码将近1K•本研究发现原内核实现有可能出现死锁，当时中断都被禁止，处理器空等待进程的运行–由于实时和并行，这种错误很难通过测试查出并排除–原来的系统错误并没有威胁到病人安全，一个原因是安装了一个限时硬件，以防控制计算机的软件或硬件错误–但这种错误有可能由于系统的修改或者升级而产生严重的后果•这里介绍简化后的这个实时内核规范2006年4月4内核基本情况这是一个典型的用于嵌入式系统的实时内核：•支持后台处理进程和中断处理器•若无中断发生，将有一个后台进程被作为当前进程，处于运行中•当前进程一直运行到自己显式释放处理器，这时调度器将选择另一进程作为当前进程•每个后台进程有一个就绪标志，调度器只在就绪进程中选择•如果一个或几个中断激活，就根据它们的优先级（用一个数表示）选出其中最紧急的中断，令相应的中断处理器运行•中断激活的条件是它们的优先级高于当时已激活的中断，当相应的处理器发出自己已结束的信号时，该中断离开激活状态•后台进程可以注册到某个优先级，使自己变成一个中断处理器图1：内核实现的数据结构（取自原文档）进程，链接成一个环中断控制下的进程调度器控制下的进程ready = trueready = false当前活动进程图2：进程状态被迫转换（其他进程导致）自主转换（自己执行命令）中断控制下的进程调度器控制下的进程箭头反了2006年4月7评价•虽然这种图很常见，但它们的信息可以为应用程序员使用的并不多，其中的许多信息与应用程序员无关，如：–中断处理器和进程连接为一个环，有就绪标志。
这些应用程序员无法检查也不可能利用–调度环只是保证后台进程按固定的顺序运行，应用程序员不能依赖这种情况（否则无法保证应用程序的稳定运行）–图中中断处理器也在环上，也有就绪标志（永远为假），实际上完全可能采用其他实现方式（例如中断处理器从环上取下等）•图2可以看作半形式化描述，把内核描述为一组有穷自动机。
但：–没有给出进程间交互的明确信息（内核需要管理的重要事项）–有些可能状态没有描述（作者举了个例子）2006年4月8内核状态下面开始用Z 做形式化描述。
首先考虑系统的状态空间进程用进程标识符指称，在内核实现中进程标识符是进程控制块的地址。
实际表示形式应用程序员不关心，可以定义为一个抽象集合：考虑定义一个唯一标识符none ，它不是真进程的名字。
当处理器闲置时可以说它正在运行进程none ，其他名字可用于真进程2006年4月9内核状态：后台进程与后台进程相关的状态与调度器有关，定义下面模式：•background ：后台进程的集合•ready ：就绪进程的集合，是调度器选择当前进程时的备选集合•current ：当前进程，可以是none 这里没有说ready 和current 之间的关系2006年4月10内核状态：中断处理器中断用与之相关的优先级表示，优先级是小整数，定义为集合（0 不是中断优先级，作为后台进程的优先级）：中断部分的状态描述为：handler 是部分单射，每个优先级关联至多一个中断处理器，互不相同enable 是允许中断级的集合，active 是当前需要处理的中断级的集合内部状态：内核对于理解内核的工作，有些信息非常关键，如：•没有允许（enable ）的中断就不能激活•不同优先级不能共享同一个处理器这些都是静态的信息，但在程序正文中并没有表现整个内核的状态就是后台和中断两部分的组合：内核状态包括6个变量：内部状态：CPU内核的工作就是确定CPU 运行哪个进程，它属于哪个优先级这两个观察应该看成系统状态的组成部分。
整个系统由CPU 和内核组成下面模式描述CPU 的状态：•当没有进程运行（CPU 运行none ）时running 的值是none •在没有激活的中断，其优先级是0•CPU 的其他状态信息与这里的规范无关（例如寄存器内容，状态寄存器的状态等等2006年4月13内部状态：系统在考虑整个系统的状态时，需要刻画CPU 状态与内核状态之间的关系•如果正在运行后台进程，当时CPU 的priority 必定为0•如果存在激活中断，CPU 一定处于其中最高的优先级，而且正在运行这个优先级的中断处理器下面是描述整个系统状态的模式：易见有：2006年4月14后台进程：启动下面考虑系统状态的变化有些操作只影响状态空间里的后台进程部分，先考虑这部分操作。
操作Start 将一个进程变为后台进程。
用下面模式描述：现有后台进程可以重新Start ，将其置于就绪状态2006年4月15后台进程：释放处理器当前后台进程可以通过调用Detach 操作释放CPU ，下面是相应模式：执行这一操作的前提是当前CPU 运行的是后台进程操作将CPU 置为闲逛状态（执行none 进程），下面的操作将是选择一个新后台进程，或者出现中断2006年4月16后台进程：选择在CPU 闲置时（运行none ），可能自发地执行选择操作。
该操作的模式：•这一操作不属于内核应用程序接口，而是内核的一个内部操作，可以在其前条件满足的情况下随时发生•其前条件是：•规范没说如何选择（抽象性），选择策略（调度策略）是实现的责任•一旦某进程被选中，它一定会立即投入运行，因为当时的优先级为0后台进程：结束后台进程可以自己执行Stop 操作终止，这个进程就结束了：•当时正在运行的必须是一个真正的后台进程•结束的进程从background 和ready 集合里删除•当前进程变为none ，又可能执行Select后台进程：设置就绪/非就绪后台进程可以在就绪和“挂起”状态之间转换，为描述设置进程状态操作，需要先定义一个枚举类型操作的规范：2006年4月19中断处理：注册现在考虑中断处理部分。
一个进程可以把自己注册为中断处理器：本操作只能由后台进程调用。
调用进程从现有后台进程集删除，并注册为指定优先级的处理器（如果原来有，就是取而代之）2006年4月20中断处理：中断处理器硬件保证只有允许的且高于当前处理器优先级的中断才能发生下面模式描述内核在发生中断时的行为：这一模式只说新中断被加入激活中断的集合静态调度模式保证与新中断相关的处理器将开始运行（由系统的priority 确定），下面推导说明新中断的处理器将开始执行：2006年4月21中断处理：新中断因此有：调度策略的其他部分保证：2006年4月22中断处理：结束当一个中断处理器工作完成时，中断处理器调用内核操作IWait ，将自己挂起等待下一次中断。
这个操作的形式描述：只有中断处理器才能执行这个操作（priority > 0）执行操作使当前中断处理器从active 集合中去除，调度策略将自动决定随后执行的中断处理器（或者后台进程）中断处理：撤销另一个操作IExit 结束中断处理器，并撤销它的注册：这个操作使该中断处理器恢复为一个后台进程。
最后两个操作修改允许中断集合，屏蔽或允许中断中断处理：屏蔽2006年4月25原实现的一个错误在原来的实现里，注册操作的实现并不是前面描述的那样，而是：注意这里current' 的定义，这一修改破坏了系统的正确性，因为现在要求必须有另一个就绪的后台进程，调度器将陷入无限循环，去寻找下一个就绪的后台进程（在调度器运行时，将禁止任何中断），导致系统死锁2006年4月26总结•本实例描述了一个实时内核的许多重要方面，但又没有陷入过多的实现细节，如具体数据结构等•这里不仅描述了一个进程执行中可能发生的事件，通过这些事件，进程也可以与其他进程交互，以及与中断交互•但也有一些重要的方面没有包含在这个规范里：–没有模拟进程的状态，进程在释放CPU 时，或者被中断时，必须保存当时的状态，在重新执行时恢复状态–并没有真的描述时间，或者特定时间发生的事件–没有关于进程的调度应该具有某种公平性的描述•其中第一个问题容易解决，只需为每个进程增加状态变量•后面两个问题更困难。
时间信息较难很好地集成在相关描述中，后来有许多人研究带时间的规范，例如有一种带时间的Z 扩充称为TCOZ2006年4月27总结•公平性无法在单一事件的层次上描述，因为它讨论的是系统的长程性质，实际上是无穷事件序列的性质问题。
也可能想出一些描述方法，关键就是重新定义Select•虽然这些问题都可能处理，但加入之后的规范将会复杂许多、难理解许多整理自：Specifying a real-time kernel, Mike Spivey, Oxford2006年4月28实例2：文本格式化工具问题简介 基本概念 文本处理 实现细节 文件 总结问题简介本实例研究描述一个文本格式化程序，它能完成：•普通的ASCII （或者其他字符集的）文本文件的格式化工作，能对各个行做居左、居中和居右的格式编排•实现对于制表符和换行的处理这一规范描述的基本上是Unix 系统里的基本工具pos ，其手册页的基本内容如下（下面的规范并不等价于这一工具。
这种写规范的方式，可以看作是想澄清原工具的各种设计问题，而不是严格的逆向工程）：2006年4月31基本概念现在考虑内容为一些ASCII 字符的文件，定义表示字符的基本集合：空格是一个特殊的字符：行和文档（document ）的抽象可定义如下：字符行是字符的序列文档是字符行的序列有时需要重复一个串若干遍，为此可以扩充Z 语言，利用其功能定义一个运算符，下面通过通用型定义引进一个新运算符2006年4月32基本概念这个定义在下面很有用。
很容易看到这一运算符的许多性质，如：2006年4月33基本概念其中两个很有用的序列运算符定义如下：运算符after 取得n 个元素之后的（子）序列运算符for 取得序列前n 个元素构成的（子）序列2006年4月34文本处理下面考虑文本处理，首先考虑行的处理，而后考虑整个文档的处理。
首先考虑一个函数clipleft ，它删除一行开始的所有空格（如果存在）删除右边所有空格的工作也可以借助上述函数实现：注意：这样描述并不意味着实现中需要这样做写规范时做的是描述操作的性质，实现是后面的工作文本处理：行很容易用它们组合出一个删除两端空格的函数：这两个操作的组合具有下面的性质（可以严格证明）：文本处理下面考虑一行内的位置编排要设定一个行的左端从某个位置开始，也就是在行的开始加入若干空格下面函数完成这一工作：如果一行不是太长，那么就可以将它居中编排，下面函数完成这一工作。