Formal analysis of the priority ceiling protocol

被引：19

作者：

Dutertre, B ^{[1
]}

机构：

[1] SRI Int, Syst Design Lab, Menlo Pk, CA 94025 USA

来源：

21ST IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS | 2000年

关键词：

D O I：

10.1109/REAL.2000.896005

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：151 / 160

页数：10

共 14 条

[1]

ALTISEN K, 2000, IN PRESS FORMAL TECH

[2]

Audsley N.C., 1991, Proc. of the 8th IEEE Workshop on Real-Time Operating Systems and Software, P127

[3]

DUTERTRE B, 1999, PRIORITY CEILING PRO

[4]

Fowler S, 1996, LECT NOTES COMPUT SC, V1135, P440