A formal proof of the deadline driven scheduler in PPTL axiomatic system
DOI10.1016/J.TCS.2013.12.014zbMATH Open1360.68771OpenAlexW2039684730MaRDI QIDQ744103FDOQ744103
Authors: Nan Zhang, Zhenhua Duan, Cong Tian, Du Ding-Zhu 
Publication date: 6 October 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2013.12.014
Recommendations
- Verifying safety critical task scheduling systems in PPTL axiom system
- An intuitive formal proof for deadline driven scheduler
- Complete axiomatization for projection temporal logic with finite time
- A complete proof system for propositional projection temporal logic
- Formalising scheduling theories in duration calculus
Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Framed temporal logic programming
- Title not available (Why is that?)
- A cylinder computation model for many-core parallel computing
- Title not available (Why is that?)
- A calculus of durations
- A decision procedure for propositional projection temporal logic with infinite models
- Automated Theorem Proving: After 25 Years
- Complexity of propositional projection temporal logic with star
- Title not available (Why is that?)
- A complete proof system for propositional projection temporal logic
- Expressiveness of propositional projection temporal logic with star
- Formalising scheduling theories in duration calculus
- An intuitive formal proof for deadline driven scheduler
Cited In (6)
- An intuitive formal proof for deadline driven scheduler
- A mechanism of function calls in MSVL
- Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis
- A sound and complete proof system for a unified temporal logic
- Efficient decision procedure for propositional projection temporal logic
- Index set expressions can represent temporal logic formulas
Uses Software
This page was built for publication: A formal proof of the deadline driven scheduler in PPTL axiomatic system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q744103)
