嵌入式系统的描述与验证 LiXi Computer Applications Lab CS Department,USTC
嵌入式系统的描述与验证 Li Xi Computer Applications Lab CS Department, USTC
Outline 》 形式化设计方法和过程 Formal System Specification 系统描述方法 Change of Partitioning HWSW- 一基于模型的方法 Partitioning 一基于语言的方法 Software Interface Hardware ·SystemC Synthesis Synthesis Synthesis -PetriNet,1960 System ·德国数学家Petri发明 Integration 0} 形式化验证 (1)Co-specification (3)Co-synthesis Model Checking How to model the system? Generate HW/SW components Create HW/SW communication 属性分析 一正确性、性能、可靠性？ (2)Partitioning (4)Co-simulation What functions go in Simulate HW/SW hardware versus software components interacting in real time llxx@ustc.edu.cn 2/112
llxx@ustc.edu.cn 2/112 Outline • 形式化设计方法和过程 • 系统描述方法 – 基于模型的方法 – 基于语言的方法 • SystemC – PetriNet，1960 • 德国数学家Petri发明 • 形式化验证 – Model Checking • 属性分析 – 正确性、性能、可靠性？
参考资料 USTC 世业 ·Peter Marwedel,TU Dortmund教授 盖入式系统设计一嵌入式 信息物理系统基础潭书南 -《嵌入式系统设计·嵌入式CPS系统基础》，第2版 ,2011 一第二章：规范与建模 ⊙ 0 Albert M.K.Cheng,休斯顿大学CSEE教授 《嵌入式实时系统：调度、分析与验证》， REAL-TIME Viley2002/北航出版社2015 SYSTEMS 面向嵌入式实时系统，较系统地论述基本的实时调 度算法、调度性分析方法，特别列举了大量关于安 全芙键系统的工程实例。 Daniel D.Gajski((盖斯基)，加大艾尔温分校 5p0000Qq -《嵌入式系统的描述与设计》，2005， 嵌人式系统的 绕芬系餐整祛模鞲褪给锁？茶僰羲渟庭学季 播述与设计 CHINA-PUB.COM
参考资料 • Peter Marwedel，TU Dortmund教授 – 《嵌入式系统设计·嵌入式CPS系统基础》，第2版 ，2011 – 第二章：规范与建模 • Albert M.K. Cheng，休斯顿大学CSEE教授 – 《嵌入式实时系统：调度、分析与验证》， Wiley2002/北航出版社2015 – 面向嵌入式实时系统，较系统地论述基本的实时调 度算法、调度性分析方法，特别列举了大量关于安 全关键系统的工程实例。 • Daniel D. Gajski(盖斯基)，加大艾尔温分校 – 《嵌入式系统的描述与设计》, 2005， – 嵌入式系统设计：模型和体系结构、描述语言、系 统划分、质量评估、描述细化以及系统级方法学等
嵌入式系统的特征 State Transitions Intrinsically state-based ·持续不断地响应外部事件，进行状态转移 ·Real Time 一正确性依赖于完成的时间 Failure to meet deadlines might create safety issues or simply unhappy customers Exceptions ·Interrupt handling is crucial,某些事件需要即时相应 Concurrency Both Task-level and Statement-level concurrency llxx@ustc.edu.cn 4/112
llxx@ustc.edu.cn 4/112 嵌入式系统的特征 • State Transitions – Intrinsically state-based • 持续不断地响应外部事件，进行状态转移 • Real Time – 正确性依赖于完成的时间 • Failure to meet deadlines might create safety issues or simply unhappy customers – Exceptions • Interrupt handling is crucial，某些事件需要即时相应 • Concurrency – Both Task-level and Statement-level concurrency
嵌入式系统的描述要求 ·并发性 ·通信 ·状态迁移 ·同步 ·层次化 ·异常 ·程序结构 ·非确定性 ·行为完成 ·时序 input outputs events transition function current next state state state llxx@ustc.edu.cn 5/112
llxx@ustc.edu.cn 5/112 嵌入式系统的描述要求 • 并发性 • 状态迁移 • 层次化 • 程序结构 • 行为完成 • 通信 • 同步 • 异常 • 非确定性 • 时序
System interface elevator controller Unit 的 Control State Transitions down apen floor req floor Request Resolver floor b1 buttons inside N elevator floor up1 up/down buttors on floor each floor dn3 floor dnN Hoistway
elevator controller • State Transitions floor floor floor floor floor Hoistway
三种描述方法：自然语言、算法、状态图 "If the elevator is stationary and the loop floor requested is equal to the if (req_floor curr_floor)then current floor,then the elevator direction idle; remains idle. elseif(req_floor curr_floor)then If the elevator is stationary and the floor requested is less than the direction :down; current floor,then lower the elseif(req_floor curr_floor)then elevator to the requested floor. direction :up; If the elevator is stationary and the end if; floor requested is greater than end loop; the current floor,then raise the elevator to the requested floor" req_floorcurr_floor req_floorcurr_floor down)reg floor=curr floor idle req_floor=curr_floor up rea floo2 curr floor小 reg floorscurr floor llxx@ustc.edu.cn 7/112
llxx@ustc.edu.cn 7/112 三种描述方法：自然语言、算法、状态图
形式化方法(Formal Method) 定义：采用离散数学的方法建立系统的精确的数学模型，并 对模型进行分析。 -运用形式化语言，进行形式化的规格描述、模型推理和验证。 o 目的：保证系统设计的正确性 保证规格说明的无二义性，使得证明和验证系统实现满足用户和系 统需求成为可能。 - 检查模型的一致性，推导模型的逻辑结果，模拟执行模型等 ● 效益 一系统代码规模 ·1979年，哥伦比亚航天飞机4000万行 ·2001年，XP3500万行，目前4000万行；Vista超过5000万行。 -非形式化技术：软件故障率2~20个/千行代码 形式化技术：软件故障率0.75个/千行代码(1992年，英国民航局信 息显示系统) llxx@ustc.edu.cn 8/112
llxx@ustc.edu.cn 8/112 形式化方法（Formal Method） • 定义：采用离散数学的方法建立系统的精确的数学模型，并 对模型进行分析。 – 运用形式化语言，进行形式化的规格描述、模型推理和验证。 • 目的：保证系统设计的正确性 – 保证规格说明的无二义性，使得证明和验证系统实现满足用户和系 统需求成为可能。 – 检查模型的一致性，推导模型的逻辑结果，模拟/执行模型等 • 效益 – 系统代码规模 • 1979年，哥伦比亚航天飞机4000万行 • 2001年， XP 3500万行，目前4000万行；Vista超过5000万行。 – 非形式化技术：软件故障率2～20个/千行代码 – 形式化技术：软件故障率0.75个/千行代码（1992年，英国民航局信 息显示系统）
离散系统(discrete system) STC 定义：系统状态只在有限的时间点或可数的时 间点上由随机事件驱动的系统 一由异步、突发的事件驱动状态演化 一行为：用其演化过程的状态序列和事件序列来刻画 ·状态变迁系统：状态通常只取有限个离散值 一系统状态的变化是在一个时间点上瞬间完成的. - 如排队系统(queue system),状态量的变化只 是在离散的随机时间点上发生. ·离散事件系统、离散事件动态系统 -事件->动作->状态 llxx@ustc.edu.cn 9/112
离散系统(discrete system) • 定义：系统状态只在有限的时间点或可数的时 间点上由随机事件驱动的系统 – 由异步、突发的事件驱动状态演化 – 行为：用其演化过程的状态序列和事件序列来刻画 • 状态变迁系统：状态通常只取有限个离散值 – 系统状态的变化是在一个时间点上瞬间完成的． – 如排队系统（queue system），状态量的变化只 是在离散的随机时间点上发生． • 离散事件系统、离散事件动态系统 – 事件->动作->状态 llxx@ustc.edu.cn 9/112
形式化开发过程 》 ·建立需求与系统模型之间的映射关系 -模型获取 ·从现实世界向模型表示的转化过程 ·形式规约 模型验证 ·判断模型表示是否符合需求 ASIC Analog I/O Processor Memory ·形式证明与验证 -模型变换 ·从模型表示向计算机系统的转化过程 一一对多关系，即一个模型对应多种实现 DSP 》一致性检查 Code ·设计求精 llxx@ustc.edu.cn 10/112
llxx@ustc.edu.cn 10/112 形式化开发过程 • 建立需求与系统模型之间的映射关系 – 模型获取 • 从现实世界向模型表示的转化过程 • 形式规约 – 模型验证 • 判断模型表示是否符合需求 • 形式证明与验证 – 模型变换 • 从模型表示向计算机系统的转化过程 – 一对多关系，即一个模型对应多种实现 » 一致性检查 • 设计求精 Processor Analog I/O Memory ASIC DSP Code