This is assessed and evaluated via a standard case study: the cardiac pacemaker. Additionally a formalisation of an Electrocardiogram (ECG) is used to identify anomalies in order to improve existing medical protocols. This allows the key issue - that formal methods are not currently integrated into established critical systems development processes - to be discussed in a highly effective and informative way.Defining a new development life-cycle methodology, together with a set of associated techniques and tools to develop highly critical systems using formal techniques, this book adopts a rigorous safety assessment approach explored via several layers.