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

DOI10.1023/B:TIME.0000027933.63133.5FMaRDI QIDQ704786zbMATH OpenOpenAlexFDO

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

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)

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

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)