A formal proof of the deadline driven scheduler in PPTL axiomatic system
DOI10.1016/j.tcs.2013.12.014zbMath1360.68771OpenAlexW2039684730MaRDI QIDQ744103
Cong Tian, Zhenhua Duan, Nan Zhang, Ding-Zhu Du
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
Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A cylinder computation model for many-core parallel computing
- A complete proof system for propositional projection temporal logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A calculus of durations
- Expressiveness of propositional projection temporal logic with star
- Framed temporal logic programming
- 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
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
- An intuitive formal proof for deadline driven scheduler
