嵌入式系统的属性与验证.pdfVIP

嵌入式系统的属性与验证 Li Xi Computer Applications Lab CS Department, USTC Outline • 形式化设计方法和过程 • 系统描述方法：基于状态和迁移 • 形式化验证 – Model Checking – 时态逻辑：LTL、CTL、RTL •• 属性分析属性分析 – 正确性、性能、可靠性？ • Peter Marwedel，TU Dortmund教授 – 《嵌入式系统设计·嵌入式CPS系统基础》，第2版2011 – 第5.8节：形式验证 • Albert M.K. Cheng ，休斯顿大学CSEE教授 – 《嵌入式实时系统：调度、分析与验证》，Wiley2002/北航出版社2015 – 面向嵌入式实时系统，较系统地论述基本的实时调度算法、调度性分析方法，特别 列举了大量关于安全关键系统的工程实例 llxx@ 2/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 llxx@ 3/112 嵌入式系统的描述要求 • 并发性 • 通信 • 状态迁移 • 同步 • 层次化 • 异常 • 程序结构 • 非确定性 •• 行为完成行为完成 •• 时序时序 • 基于状态：FSM • 基于动作：CFG，DFG （KPN，SDF ） llxx@ 4/112 形式化方法 （Formal Method） • 定义： – 用离散数学的方法建立系统的精确数学模型，并对模型进行分析。 • 集合论、图论、代数结构、组合数学、数理逻辑。。。 – 运用形式化语言，进行形式化的规格描 、模型推理和验证。 • 目的：保证系统设计的正确性 – 保证规格说明的无二义性 •• 使得证明和验证系统实现满足用户和系统需求成为可能使得证明和验证系统实现满足用户和系统需求成为可能。。 – 检查模型的一致性，推导模型的逻辑结果，模拟/执行模型等 • 效益 – 系统代码规模 • 1979年，哥伦比亚航天飞机4000万行 （2001年，XP 3500万行） – 非形式化技术：软件故障率2～20个/千行代码 – 形式化技术：软件故障率0.75个/千行代码 （1992年，英国民航局信 息显示系统） llxx@ 5/112 形式化开发过程 • 建立需求与系统模型之间的映射关系 – 模型获取 • 从现实世界向模型表示的转化过程