An engineering process for the verification of real-time systems

DOI10.1007/s00165-006-0021-4zbMath1111.68076OpenAlexW2114443848MaRDI QIDQ877159

N. E. Zubov

Publication date: 19 April 2007

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-006-0021-4

zbMATH Keywords

Model checkingAda95Ravenscar profileRely/guarantee conditionsScheduling analysisSPARKUPPAAL

Mathematics Subject Classification ID

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

Uses Software

• Ada95
• SPARK
• Uppaal

Cites Work

• Uppaal in a nutshell
• On the complexity of fixed-priority scheduling of periodic, real-time tasks
• Bounds on Multiprocessing Timing Anomalies
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item