Combined Formal Refinement and Model Checking for Real-Time Systems Verification
Alexander Krupp, Wolfgang Müller, Ian Oliver · Kluwer Academic Publishers eBooks · 2006
We present a framework, which combines model checking and theorem prover based refinement for real-time systems design focusing on the refinement of non deterministic to timed deterministic finite state machines. Our verification flow starts from a cycle accurate finite state machine for the RAVEN model checker. We present a translation, which transforms the model into efficient B language code. After refining the RAVEN model and annotating it, the time accurate model is also translated to B so that the B theorem prover can verify the refined model almost automatically. The approach is introduced by the example of a mobile phone echo cancellation unit.