Verifying safety critical task scheduling systems in PPTL axiom system

Nan Zhang, Mengfei Yang, Bin Gu, Zhenhua Duan () and Cong Tian
Additional contact information
Nan Zhang: Xidian University
Mengfei Yang: China Academy of Space Technology
Bin Gu: China Academy of Space Technology
Zhenhua Duan: Xidian University
Cong Tian: Xidian University

Journal of Combinatorial Optimization, 2016, vol. 31, issue 2, No 8, 577-603

Abstract: Abstract 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.

Keywords: Theorem proving; Scheduler; Real-time; Safety critical system (search for similar items in EconPapers)
Date: 2016
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
http://link.springer.com/10.1007/s10878-014-9776-3 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:jcomop:v:31:y:2016:i:2:d:10.1007_s10878-014-9776-3

Ordering information: This journal article can be ordered from
https://www.springer.com/journal/10878

DOI: 10.1007/s10878-014-9776-3

Access Statistics for this article

Journal of Combinatorial Optimization is currently edited by Thai, My T.

More articles in Journal of Combinatorial Optimization from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().