Combining Formal Refinement and Model Checking for Real-Time Systems Verification.
Alexander Krupp, Wolfgang Müller · 2003
We present a framework which combines model checking and theorem prover based refinement for the design of real-time systems focusing on the refinement step when annotating the state-oriented model with timing information. Our verification flow starts from a cycle-accurate finite state machine for the RAVEN model checker and present a translation which efficiently transforms the model to the B language. After refining the RAVEN model and annoting it, the time-accurate model is also translated to B so that the B theorem prover can verify the refinement almost automatically. The experimental results demonstrate that the presented solution requires almost no user interaction and results in most efficient runtimes when applying the Atelier-B theorem prover.