Real-Time Trigger-Response Properties for Event-B Applied to the Pacemaker

As the physical world evolves with time, safety-critical systems are usually used with time-dependent functionality. The design and implementation of real-time systems are challenging due to the complicated functional and timing requirements. Event - B formalization offers a stepwise development approach for specifying and verifying systems with mathematical techniques and tools. In this paper, we...