嵌入式系统的描述与验证 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 嵌入式系统的描述要求 • 并发性 • 状态迁移 • 层次化 • 程序结构 • 行为完成 • 通信 • 同步 • 异常 • 非确定性 • 时序