A formal proof of the deadline driven scheduler in PPTL axiomatic system
type: Item
instance of: scholarly article
title: A formal proof of the deadline driven scheduler in PPTL axiomatic system
zbMATH Open document ID: 1360.68771
author: Nan Zhang
author: Zhenhua Duan
author: Cong Tian
author: Du Ding-Zhu
published in: Theoretical Computer Science
publication date: 2014-10-06T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68M20
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 6351437
zbMATH Keywords: theorem proving
zbMATH Keywords: projection temporal logic
zbMATH Keywords: deadline driven scheduler
zbMATH Keywords: real-time system
describes a project that uses: PVS
describes a project that uses: ACL2
describes a project that uses: SPIN
describes a project that uses: CESAR
MaRDI profile type: Publication
full work available at URL: j.tcs.2013.12.014
OpenAlex ID: W2039684730
cites work: Q3336675
cites work: Q3940830
cites work: Automated Theorem Proving: After 25 Years
cites work: Q3141897
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Q3703866
cites work: Expressiveness of propositional projection temporal logic with star
cites work: Framed temporal logic programming
cites work: Q3806791
cites work: A cylinder computation model for many-core parallel computing
cites work: A complete proof system for propositional projection temporal logic
cites work: Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
cites work: A calculus of durations
cites work: An intuitive formal proof for deadline driven scheduler
cites work: Q3181698
cites work: Complexity of propositional projection temporal logic with star
cites work: A decision procedure for propositional projection temporal logic with infinite models
DOI: 10.1016/J.TCS.2013.12.014
description: scientific article; zbMATH DE number 6351437