Using program transformations to provide safety properties for real-time systems

DOI10.1023/B:TIME.0000027933.63133.5FzbMATH Open1101.68057OpenAlexW2089018547MaRDI QIDQ704786FDOQ704786

Authors: Grace Tsai, Shuhua Wang 

Publication date: 19 January 2005

Published in: Real-Time Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/b:time.0000027933.63133.5f

Recommendations

• Verification of schedulability for real-time programs
• A compositional framework for fault tolerance by specification transformation
• Verification, refinement and scheduling of real-time programs
• Specification and compositional verification of real-time systems
• An algebraic approach for compiling real-time programs

zbMATH Keywords

fault toleranceformal methodstemporal logicprogram verificationexecutable assertionsReal time systems

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (3)

• Verification of schedulability for real-time programs
• Verification of a controller for BART: An approach based on Horn logic and denotational semantics
• Refining the Safety-Liveness Classification of Temporal Properties According to Realizability

This page was built for publication: Using program transformations to provide safety properties for real-time systems

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