zbMATH — the first resource for mathematics

Verifying safety critical task scheduling systems in PPTL axiom system. (English) Zbl 1333.90055
Summary: This paper presents a case study of formal verification of safety critical task scheduling systems. First, a scheduling algorithm described in a temporal logic programming language is presented; then a sufficient and necessary condition for the schedulability of task set is formalized. Further, the correctness of the condition is proved by means of theorem proving in the axiom system of Propositional Projection Temporal Logic.

MSC:
 90B35 Deterministic scheduling theory in operations research
Software:
ML ; Isabelle; SPIN; HOL; ACL2; PVS
Full Text:
References:
 [1] Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Springer-Verlag, Berlin, Heidelberg · Zbl 1161.03008 [2] Brock B, Kaufmann M, Moore J (1996) Acl2 theorems about commercial microprocessors. In: Srivas M, Camilleri A (eds) Proceedings of the 1st international conference on formal methods in computer-aided design. Springer-Verlag, London, pp 275-293 [3] Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Beijing [4] Duan, Z; Zhang, N; Koutny, M, A complete proof system for propositional projection temporal logic, Theoret Comput Sci, 497, 84-107, (2013) · Zbl 1417.03146 [5] Gordon M, Melham T (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge · Zbl 0779.68007 [6] Holzmann, G, The model checker spin, IEEE Trans Softw Eng, 23, 279-295, (1997) [7] McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer Academic, Dordrecht [8] Owre S, Rushby J (1992) Pvs: a prototype verification system. In: Kapur D (ed) Proceedings of the 11th international conference on automated deduction. Springer-Verlag, Heidelberg, pp 748-752 · Zbl 0534.03009 [9] Paulson L (1994) Isabelle—a generic theorem prover. Springer, Berlin · Zbl 0825.68059 [10] Sistla A (1983) Theoretical issues in the design and verification of distributed systems. PhD thesis, Harvard University [11] Tian, C; Duan, Z, Complexity of propositional projection temporal logic with star, Math Str Comput Sci, 19, 73-100, (2009) · Zbl 1161.03008 [12] Vardi M (1988) A temporal fixpoint calculus. In: POPL ’88 Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, pp 250-259 [13] Wolper, P, Temporal logic can be more expressive, Info Control, 56, 72-99, (1983) · Zbl 0534.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.