恩 嵌入式系统的属性与验证 LiXi Computer Applications Lab CS Department,USTC
嵌入式系统的属性与验证 Li Xi Computer Applications Lab CS Department, USTC
Fommal System Specification Outline Change of Partitioning HWSW- Partitioning 形式化设计方法和过程 Software Interface Hea小ware Synthesis Synthesis Synthesis 系统描述方法：基于状态和迁移 System 形式化验证 Integration - Model Checking -时态逻辑：LTL、CTL、RTL ·属性分析 一正确性、性能、可靠性？ ·Peter Marwedel,TU Dortmund教授 REAL-TIME SYSTEMS 《嵌入式系统设计·嵌入式CPS系统基础》，第2版2011 第5.8节：形式验证 ·Albert M.K.Cheng,休斯顿大学CSEE教授 《嵌入式实时系统：调度、分析与验证》，Viley2002/北航出版社2015 面向嵌入式实时系统，较系统地论述基本的实时调度算法、调度性分析方法，特别 列举了大量关于安全关键系统的工程实例 llxx@ustc.edu.cn 2/112
Outline • 形式化设计方法和过程 • 系统描述方法：基于状态和迁移 • 形式化验证 – Model Checking – 时态逻辑：LTL、CTL、RTL • 属性分析 llxx@ustc.edu.cn 2/112 – 正确性、性能、可靠性？ • Peter Marwedel，TU Dortmund教授 – 《嵌入式系统设计·嵌入式CPS系统基础》，第2版2011 – 第5.8节：形式验证 • Albert M.K. Cheng，休斯顿大学CSEE教授 – 《嵌入式实时系统：调度、分析与验证》，Wiley2002/北航出版社2015 – 面向嵌入式实时系统，较系统地论述基本的实时调度算法、调度性分析方法，特别 列举了大量关于安全关键系统的工程实例
实时嵌入式系统的特征 State Transitions input outputs events Intrinsically state-based transition function ·持续不断地响应外部事件，进行状态转移 current next state state 。Real Time state 正确性依赖于完成的时间 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 3/112
实时嵌入式系统的特征 • State Transitions – Intrinsically state-based • 持续不断地响应外部事件，进行状态转移 • Real Time – 正确性依赖于完成的时间 llxx@ustc.edu.cn 3/112 • 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
嵌入式系统的描述要求 ·并发性 ·通信 ·状态迁移 ·同步 ·层次化 ·异常 ·程序结构 ·非确定性 ·行为完成 ·时序 亚皿有 ·基于状态：FSM ·基于动作：CFG,DFG(KPN,SDF) llxx@ustc.edu.cn 4/112
嵌入式系统的描述要求 • 并发性 • 状态迁移 • 层次化 • 程序结构 • 行为完成 • 通信 • 同步 • 异常 • 非确定性 • 时序 llxx@ustc.edu.cn 4/112 • 行为完成 • 基于状态：FSM • 基于动作：CFG，DFG（KPN，SDF） • 时序
形式化方法(Formal Method) ·定义： 一用离散数学的方法建立系统的精确数学模型，并对模型进行分析。 ·集合论、图论、代数结构、组合数学、数理逻辑。。。 一运用形式化语言，进行形式化的规格描述、模型推理和验证。 ● 目的：保证系统设计的正确性 -保证规格说明的无二义性 ·使得证明和验证系统实现满足用户和系统需求成为可能。 -检查模型的一致性，推导模型的逻辑结果，模拟/执行模型等 。 效益 一系统代码规模 ·1979年，哥伦比亚航天飞机4000万行(2001年，XP3500万行) -非形式化技术：软件故障率2~一20个/千行代码 -形式化技术：软件故障率0.75个/千行代码(1992年，英国民航局信 息显示系统) llxx@ustc.edu.cn 5/112
形式化方法（Formal Method） • 定义： – 用离散数学的方法建立系统的精确数学模型，并对模型进行分析。 • 集合论、图论、代数结构、组合数学、数理逻辑。。。 – 运用形式化语言，进行形式化的规格描述、模型推理和验证。 • 目的：保证系统设计的正确性 – 保证规格说明的无二义性 • 使得证明和验证系统实现满足用户和系统需求成为可能。 llxx@ustc.edu.cn 5/112 • 使得证明和验证系统实现满足用户和系统需求成为可能。 – 检查模型的一致性，推导模型的逻辑结果，模拟/执行模型等 • 效益 – 系统代码规模 • 1979年，哥伦比亚航天飞机4000万行（2001年， XP 3500万行） – 非形式化技术：软件故障率2～20个/千行代码 – 形式化技术：软件故障率0.75个/千行代码（1992年，英国民航局信 息显示系统）