恩 嵌入式系统的属性与验证 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年，英国民航局信 息显示系统）
形式化开发过程 ·建立需求与系统模型之间的映射关系 -模型获取 Requirement △△△ ·从现实世界向模型表示的转化过程 capture ·形式规约 System 一模型验证 modelling ·判断模型表示是否符合需求 System ·形式证明与验证 synthesis -模型变换 ·从模型表示向计算机系统的转化过程 一一对多关系，即一个模型对应多种实现 》一致性检查 ·设计求精 llxx@ustc.edu.cn 6/112
形式化开发过程 • 建立需求与系统模型之间的映射关系 – 模型获取 • 从现实世界向模型表示的转化过程 • 形式规约 – 模型验证 llxx@ustc.edu.cn 6/112 • 判断模型表示是否符合需求 • 形式证明与验证 – 模型变换 • 从模型表示向计算机系统的转化过程 – 一对多关系，即一个模型对应多种实现 » 一致性检查 • 设计求精
规格说明技术 USTC 。 描述系统对象，对象的操作方法，以及对象的行为 -非形式化方法，称“规格说明” 一形式化方法，称“形式规约” 形式规约(Formal Specification) -描述类 ·基于数学公理和概念，通过逻辑或代数，给出系统的状态空 间，采用自动工具进行验证。 -基于代数的方法：Z、VDM、Larch -基于逻辑：一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) 一操作类：操作语义 ·基于状态和迁移，通过可执行模型描述系统，采用静态分析 和模型执行进行验证。 -基于模型：图示化，直观 一基于语言：程序，一种可执行的形式规约 llxx@ustc.edu.cn 7/112
规格说明技术 • 描述系统对象，对象的操作方法，以及对象的行为 – 非形式化方法，称“规格说明” – 形式化方法，称“形式规约” • 形式规约（Formal Specification） – 描述类 • 基于数学公理和概念，通过逻辑或代数，给出系统的状态空 llxx@ustc.edu.cn 7/112 • 基于数学公理和概念，通过逻辑或代数，给出系统的状态空 间，采用自动工具进行验证。 – 基于代数的方法：Z、VDM、Larch – 基于逻辑：一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) – 操作类：操作语义 • 基于状态和迁移，通过可执行模型描述系统，采用静态分析 和模型执行进行验证。 – 基于模型：图示化，直观 – 基于语言：程序，一种可执行的形式规约
形式证明与验证(Formal Verification&Validation) ,定理证明：可以处理无限状态空间问题 -演绎验证(deductive verification) ·采用逻辑公式表示系统规约及其性质 -工具（定理证明器，Theorem Prover) ·用户引导自动推演工具：ACL2、LP、Eves ·证明检验器：HOL、LCF、LEGO ·符合证明器：PVS ·基于分离逻辑+交互式证明：Coq 模型检验model--checking:适用于有穷状态系统 -完全自动化，验证速度快 ·检验性质不满足时，给出反例。 ·状态空间爆炸 一工具 ·时态逻辑模型检验工具：SMV/NuSMV、SPIN、UPPAAL ·行为一致性检验工具：FDR、Cospan/Formal Checker ·复合检验工具：HSIS、METAFrame 8/112
形式证明与验证(Formal Verification & Validation) • 定理证明：可以处理无限状态空间问题 – 演绎验证（deductive verification） • 采用逻辑公式表示系统规约及其性质 – 工具（定理证明器，Theorem Prover） • 用户引导自动推演工具：ACL2、LP、Eves • 证明检验器：HOL、LCF、LEGO • 符合证明器：PVS 8/112 • 符合证明器：PVS • 基于分离逻辑+交互式证明：Coq • 模型检验model-checking：适用于有穷状态系统 – 完全自动化，验证速度快 • 检验性质不满足时，给出反例。 • 状态空间爆炸 – 工具 • 时态逻辑模型检验工具：SMV/NuSMV、SPIN 、UPPAAL • 行为一致性检验工具：FDR、Cospan/Formal Checker • 复合检验工具：HSIS、METAFrame
模型检测原理：dual-language approach Yes or Real-world system Finite-state model X No Model checker AGb1ow吧 Desired property Logic formula more detailed 工 more abstract “implementation" “specification'" (system model) (system property) 'satisfies","implements","refines" (satisfaction relation)
模型检测原理：dual-language approach 9/112
Model checking (dual-language approacm is a technique for verifying finite state concurrent systems 实际系统 需求 建模 形式化 -Modeling 模型 规范 Convert a design into a formalism 修改 -Automata 模型检测器 Yes No -Specification 反例 结束 State the properties that design must satisfy SPECs are written in propositional temporal logic. Verification Check whether the properties is preserved Verification procedure is an exhaustive search of the state space of the design. If no,a counterexample raises llxx@ustc.edu.cn 10/112
Model checking (dual-language approach) • is a technique for verifying finite state concurrent systems – Modeling • Convert a design into a formalism – Automata llxx@ustc.edu.cn 10/112 – Specification • State the properties that design must satisfy – SPECs are written in propositional temporal logic. – Verification • Check whether the properties is preserved – Verification procedure is an exhaustive search of the state space of the design. • If no, a counterexample raises