Verifying a scheduling protocol of safety-critical systems

Meng Wang (), Cong Tian (), Nan Zhang (), Zhenhua Duan () and Hongwei Du ()
Additional contact information
Meng Wang: Xidian University
Cong Tian: Xidian University
Nan Zhang: Xidian University
Zhenhua Duan: Xidian University
Hongwei Du: Harbin Institute of Technology Shenzhen Graduate School

Journal of Combinatorial Optimization, 2019, vol. 37, issue 4, No 6, 1215 pages

Abstract: Abstract It is of great importance to ensure safety and reliability of the scheduling protocol of safety-critical systems since the failure will cause serious damage. This paper analyzes a real-time scheduling protocol of a safety-critical system and models it using a Modeling, Simulation and Verification Language program. Further, the schedulability and other desired properties are specified using Propositional Projection Temporal Logic formulas. As a result, these properties are proved with theorem proving and further verified using the runtime verification approach at code level.

Keywords: Safety-critical systems; Scheduling protocol; Schedulability; Theorem proving; Model checking (search for similar items in EconPapers)
Date: 2019
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s10878-018-0343-1 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:37:y:2019:i:4:d:10.1007_s10878-018-0343-1

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

DOI: 10.1007/s10878-018-0343-1

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 ().