摘要：Scade是一种广泛用于安全关键嵌入式控制软件开发的著名商业工具，其建模语言是一种同步语言，扩展自同步数据流语言Lustre。L2C可信编译器是经过形式化验证的类Scade建模语言到C语言高可信编译器长线项目之一，与同类工作相比其源语言特性更接近于Scade建模语言。本文涉及L2C可信编译器前端设计的一个重要环节，即时钟分析/检查过程的构造与验证。主要介绍分析/检查过程所采用的时钟分析/检查规则，并探讨其验证框架。
文章目录
1 引言
2 源语言及时钟相关特性
3 时钟演算规则
3.1 面向时钟演算类型系统定义的时钟表达式
3.1.1 基本时钟表达式
3.1.2 复合时钟表达式
3.1.3 常量时钟表达式
3.1.4 特殊时钟表达式
3.2 用于时钟演算类型系统定义的时钟环境
3.3 定义时钟演算规则
3.3.1 用户定义算子声明的时钟演算规则
3.3.2 局部声明的时钟演算规则
3.3.3 等式的时钟演算规则
3.3.4 控制块的时钟演算规则
3.3.5 表达式的时钟演算规则
4 时钟分析/检查过程的验证
5 相关工作
结束语
