000			03159nam a22005297a 4500
001			sulb-eb0021686
003			BD-SySUS
005			20160413122155.0
007			cr nn 008mamaa
008			130620s2013 xxk| s |||| 0|eng d
020			_a9781447152606 _9978-1-4471-5260-6
024	7		_a10.1007/978-1-4471-5260-6 _2doi
050		4	_aQA8.9-QA10.3
072		7	_aUYA _2bicssc
072		7	_aMAT018000 _2bisacsh
072		7	_aCOM051010 _2bisacsh
082	0	4	_a005.131 _223
100	1		_aSingh, Neeraj Kumar. _eauthor.
245	1	0	_aUsing Event-B for Critical Device Software Systems _h[electronic resource] / _cby Neeraj Kumar Singh.
264		1	_aLondon : _bSpringer London : _bImprint: Springer, _c2013.
300			_aXVIII, 326 p. _bonline resource.
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
347			_atext file _bPDF _2rda
505	0		_aPreface -- Introduction -- Background -- The Modelling Framework: Event-B -- Critical System Development Methodology -- Real-Time Animator and Requirements Traceability -- Refinement Chart -- EB2ALL: An Automatic Code Generator Tool -- Formal Logic Based Heart-Model -- The Cardiac Pacemaker -- Electrocardiogram (ECG) -- Conclusion -- Appendix A: Certification Standards -- Index.
520			_aDefining 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 (from  requirements analysis to automatic source code generation). 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. Using Event-B for Critical Device Software Systems serves as a valuable resource for researchers and students of formal methods. The assessment of critical systems development is applicable to all industries, but engineers and physicians from the health domain will find the cardiac pacemaker case study of particular value.
650		0	_aComputer science.
650		0	_aHealth informatics.
650		0	_aComputer programming.
650		0	_aSoftware engineering.
650		0	_aMathematical logic.
650		0	_aComputer simulation.
650	1	4	_aComputer Science.
650	2	4	_aMathematical Logic and Formal Languages.
650	2	4	_aSoftware Engineering.
650	2	4	_aHealth Informatics.
650	2	4	_aSimulation and Modeling.
650	2	4	_aProgramming Techniques.
710	2		_aSpringerLink (Online service)
773	0		_tSpringer eBooks
776	0	8	_iPrinted edition: _z9781447152590
856	4	0	_uhttp://dx.doi.org/10.1007/978-1-4471-5260-6
912			_aZDB-2-SCS
942			_2Dewey Decimal Classification _ceBooks
999			_c43778 _d43778