Verification, refinement and scheduling of real-time programs

DOI10.1016/S0304-3975(00)00091-8MaRDI QIDQ1589590zbMATH OpenOpenAlexFDO

Authors Mathai Joseph, Zhiming Liu

Publication date 12 December 2000

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(00)00091-8

zbMATH Keywords

feasibilityreal-time programrefinementschedulabilityspecification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of schedulability for real-time programs
• Specification and compositional verification of real-time systems
• A sequential real-time refinement calculus
• Real time programming. Languages, specification and verification.
• scientific article; zbMATH DE number 2088653

Cites work

• A calculus of durations
• A calculus of refinements for program derivations
• Formal verification of parallel programs
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Reasoning about programs by exploiting the environment
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
• Specification and compositional verification of real-time systems
• Temporal proof methodologies for timed transition systems
• The existence of refinement mappings
• Verification of schedulability for real-time programs

Cited in

(12)

• Refinement of trace abstraction for real-time programs
• Verification of schedulability for real-time programs
• Schedulability analysis of fixed-priority systems using timed automata
• Verification of the legOS scheduler using Uppaal
• scientific article; zbMATH DE number 1104387 (Why is no real title available?)
• scientific article; zbMATH DE number 1949600 (Why is no real title available?)
• Runtime verification of embedded real-time systems
• Verification and parameter synthesis for real-time programs using refinement of trace abstraction
• Refinement-Based Verification of Interactive Real-Time Systems
• Using program transformations to provide safety properties for real-time systems
• Verifying time partitioning in the DEOS scheduling kernel
• Formal verification of real-time systems with preemptive scheduling

This page was built for publication: Verification, refinement and scheduling of real-time programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1589590)