Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification
Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification
复制标题
普遍系统验证背景下的现实最坏情况执行时间分析
DOI：
10.1007/978-3-540-71322-7_3
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
W. Paul
中科院分区：
文献类型：
--
作者：
Steffen Knapp;W. Paul
我们描述了一个FlexRay类总线接口的门级设计。将该接口集成到已验证的VAMP处理器的设计中，得到一个电子控制单元（ECU），通过一条公共总线将多个这样的ECU连接起来，得到一个时间触发的分布式实时系统。我们定义了这样一个系统的编程模型在指令集架构（伊萨）的水平，并证明它是正确地实现在门级。该证明将处理器正确性，通信系统，程序正确性和实际最坏情况执行时间（WCET）分析的理论结合到一个统一的数学理论中。
We describe a gate level design of a FlexRay-like bus interface. An electronic control unit (ECU) is obtained by integrating this interface into the design of the verified VAMP processor.We get a time triggered distributed real-time system by connecting several such ECU's via a common bus. We define a programming model for such a system at the instruction set architecture (ISA) level and prove that it is correctly implemented at the gate level. The proof combines theories of processor correctness, communication systems, program correctness and realistic worst-case execution time (WCET) analysis into a single unified mathematical theory.