A formal proof of the deadline driven scheduler in PPTL axiomatic system

DOI10.1016/J.TCS.2013.12.014MaRDI QIDQ744103zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

theorem provingreal-time systemdeadline driven schedulerprojection temporal logic

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 4076583 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• A calculus of durations
• A complete proof system for propositional projection temporal logic
• A cylinder computation model for many-core parallel computing
• A decision procedure for propositional projection temporal logic with infinite models
• An intuitive formal proof for deadline driven scheduler
• Automated Theorem Proving: After 25 Years
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Complexity of propositional projection temporal logic with star
• Expressiveness of propositional projection temporal logic with star
• Formalising scheduling theories in duration calculus
• Framed temporal logic programming
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment

Cited in

(8)

• Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis
• A mechanism of function calls in MSVL
• Modeling and verification of processes scheduling based on projection temporal logic for multi-core CPUs
• 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
• Verifying safety critical task scheduling systems in PPTL axiom system
• An intuitive formal proof for deadline driven scheduler

Describes a project that uses

Uses Software

• ACL2
• SPIN
• PVS
• CESAR

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)