Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

Franck Cassez, Peter Gjøl Jensen, Kim Guldstrand Larsen

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discr…