规格说明技术 对系统对象，对象的操作方法，以及对象的行为的 描述 一非形式化方法，称“规格说明” 一形式化方法，称“形式规约” 。 形式规约(Formal Specification) -描述类 ·基于数学公理和概念，通过逻辑或代数给出系统的状态空间，采 用自动工具进行验证。 -基于代数的方法：Z、VDM、Larch -基于逻辑的方法：一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) 操作类 ·基于状态和转移，通过可执行模型描述系统，采用静态分析和模 型执行进行验证。 一基于模型：图示化，直观 一基于语言：程序，一种可执行的形式规约 llxx@ustc.edu.cn 11/112
llxx@ustc.edu.cn 11/112 规格说明技术 • 对系统对象，对象的操作方法，以及对象的行为的 描述 – 非形式化方法，称“规格说明” – 形式化方法，称“形式规约” • 形式规约（Formal Specification） – 描述类 • 基于数学公理和概念，通过逻辑或代数给出系统的状态空间，采 用自动工具进行验证。 – 基于代数的方法：Z、VDM、Larch – 基于逻辑的方法：一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) – 操作类 • 基于状态和转移，通过可执行模型描述系统，采用静态分析和模 型执行进行验证。 – 基于模型：图示化，直观 – 基于语言：程序，一种可执行的形式规约
嵌入式系统的描述要求 ·并发性 ·通信 ·状态迁移 ·同步 ·层次化 异常 ·程序结构 ·非确定性 ·行为完成 ·时序 llxx@ustc.edu.cn 12/112
llxx@ustc.edu.cn 12/112 嵌入式系统的描述要求 • 并发性 • 状态迁移 • 层次化 • 程序结构 • 行为完成 • 通信 • 同步 • 异常 • 非确定性 • 时序
Petri网：并发、异步、不确定性 。 经典Petri网：是一个双重有向图(a bipartite graph) -节点：库所(Place,圆圈)，变迁(Transition,方框或短线) ·输入库所，输出库所 ·源变迁：没有输入库所的变迁 place ·阱变迁：没有输出库所的变迁 ·库所的容量函数，变迁的权函数（关联函数） Transition 一有向弧：库所节点与变迁节点之间的连接。 ·库所节点之间、变迁节点之间不能有有向弧 Token -token(黑点)：在任何时刻，库所当中包含零个或者多个 no global synchronization assumed(message passing only) 。 特例 - 基本网（条件/事件网）：库所容量为1，状态/条件/资源：变迁权为1，事件 普通网(Place/transition nets,位置/迁移网)：库所容量为无穷，变迁权为1 cl task1 task2 c3 llxx@ustc.edu.cn
• 经典Petri网：是一个双重有向图(a bipartite graph) – 节点：库所(Place，圆圈)，变迁(Transition，方框或短线) • 输入库所，输出库所 • 源变迁：没有输入库所的变迁 • 阱变迁：没有输出库所的变迁 • 库所的容量函数，变迁的权函数（关联函数） – 有向弧：库所节点与变迁节点之间的连接。 • 库所节点之间、变迁节点之间不能有有向弧 – token（黑点）：在任何时刻，库所当中包含零个或者多个 – no global synchronization assumed (message passing only) • 特例 – 基本网（条件/事件网）：库所容量为1，状态/条件/资源；变迁权为1，事件 – 普通网(Place/transition nets，位置/迁移网)：库所容量为无穷，变迁权为1 llxx@ustc.edu.cn 13/112 Petri网：并发、异步、不确定性
状态转换-变迁的实施(firing) 》 标记(marking):某时刻各库所中token的分布状况 一用来描述系统的状态。 - 设初态为MO。在标记M下，库所p中的token数量记为M(p); ·变迁的就绪 -变迁t称作就绪的，当且仅当t的每个输入库所都包含至少一个token: -源变迁的使能是无条件的。 。 变迁t实施：发生了某些事件，造成状态迁移 一（基本网/普通网）：t从每个输入库所p中消耗一个token,并为每个输出库所 p产生一个token。 源变迁的引发只会产生令牌，而不消耗任何令牌 阱变迁的引发只会消耗令牌，而不产生任何新的令牌 H 状态转换： H20 H20 02 llxx@ustc.edu.cn 14/112
llxx@ustc.edu.cn 14/112 状态转换－变迁的实施(firing) • 标记(marking)：某时刻各库所中token的分布状况 – 用来描述系统的状态。 – 设初态为M0。在标记M 下, 库所p 中的token 数量记为M ( p) ; • 变迁的就绪 – 变迁 t 称作就绪的，当且仅当 t 的每个输入库所都包含至少一个token； – 源变迁的使能是无条件的。 • 变迁 t 实施：发生了某些事件，造成状态迁移 – (基本网/普通网)：t 从每个输入库所 p中消耗一个token，并为每个输出库所 p 产生一个token。 – 源变迁的引发只会产生令牌，而不消耗任何令牌 – 阱变迁的引发只会消耗令牌，而不产生任何新的令牌 状态转换：
事件（迁移）的基本关系（并发性？ 顺序性 taskl c2 task2 c3 分支，同步 与分支 与合并 c? task1 cl AND-spit AND-join c3 task2 CS 或分支 或合并 选择性（不确定性） t11 c2 task1 21 cl CO+ OR-spit OR-join+ t12 c3 task2 cs t22+ llxx@ustc.edu.cn 15/112
llxx@ustc.edu.cn 15/112 事件(迁移)的基本关系（并发性？） 顺序性 分支，同步 选择性（不确定性）