嵌入式系统的描述与验证
Li Xi Computer Applications Lab CS Department, USTC
Outline
?? 形式化设计方法和过程 ?? 系统描述方法
– 基于模型的方法 – 基于语言的方法
?? SDL ?? SystemC ?? UML
?? 形式化验证
– Model Checking
?? 属性分析（性能、正确性、可靠性？） ?? Conclusion
llxx@ustc.edu.cn 2/80
嵌入式系统的特征
?? 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 3/80
嵌入式系统的描述要求
?? ?? ?? ?? ?? 并发性 状态迁移 层次化 程序结构 行为完成 ?? ?? ?? ?? ?? 通信 同步 异常 非 性 时序
llxx@ustc.edu.cn
4/80
设计方法学
?? 捕获－模拟
– Capture：从系统的初步结构开始设计 – Simulate：对功能、时延、故障覆盖率等进行验证
?? 描述－综合
– Describe：从描述系统行为开始设计 – Synthesize：自动综合
?? Allocation： 寄存器级组件或资源数量
– 完成“代价——性能”的权
?? Scheduling：将行为划分成控制步， 每个控制步的操作 ?? Binding：将变量分配到存储单元，操作分配到功能部件
?? 描述－搜索－细化
– 采用可执行的设计描述 – 设计空间搜索 – 细化系统实现
llxx@ustc.edu.cn 5/80
三种描述方法：自然语言、算法、状态图
llxx@ustc.edu.cn
6/80
形式化方法（Formal Method）

下一页