Formal analysis of the priority ceiling protocol
Formal analysis of the priority ceiling protocol
复制标题
DOI：
10.1109/real.2000.896005
复制
发表时间：
2000-11
期刊：
影响因子：
--
通讯作者：
B. Dutertre
中科院分区：
文献类型：
--
作者：
B. Dutertre
我们提出了一个案例研究的形式化规范和工具辅助验证的实时嵌入式系统，优先级上限协议的基础上。从操作规范的协议，我们得到严格的同步和定时性能的证明，我们得出一个可扩展性的结果零星的任务。
We present a case study in formal specification and tool-assisted verification of real-time schedulers, based on the priority ceiling protocol. Starting from operational specifications of the protocol, we obtain rigorous proofs of both synchronization and timing properties, and we derive a schedulability result for sporadic tasks.