Using Event-B for Critical Device Software Systems (Record no. 52821)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 03129nam a22005295i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 978-1-4471-5260-6 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20200420221255.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 130620s2013 xxk| s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| ISBN | 9781447152606 |
| -- | 978-1-4471-5260-6 |
| 082 04 - CLASSIFICATION NUMBER | |
| Call Number | 005.131 |
| 100 1# - AUTHOR NAME | |
| Author | Singh, Neeraj Kumar. |
| 245 10 - TITLE STATEMENT | |
| Title | Using Event-B for Critical Device Software Systems |
| 300 ## - PHYSICAL DESCRIPTION | |
| Number of Pages | XVIII, 326 p. |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Remark 2 | Preface -- 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 ## - SUMMARY, ETC. | |
| Summary, etc | 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 (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. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | http://dx.doi.org/10.1007/978-1-4471-5260-6 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | eBooks |
| 264 #1 - | |
| -- | London : |
| -- | Springer London : |
| -- | Imprint: Springer, |
| -- | 2013. |
| 336 ## - | |
| -- | text |
| -- | txt |
| -- | rdacontent |
| 337 ## - | |
| -- | computer |
| -- | c |
| -- | rdamedia |
| 338 ## - | |
| -- | online resource |
| -- | cr |
| -- | rdacarrier |
| 347 ## - | |
| -- | text file |
| -- | |
| -- | rda |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Health informatics. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Computer programming. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Software engineering. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Mathematical logic. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Computer simulation. |
| 650 14 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Mathematical Logic and Formal Languages. |
| 650 24 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Software Engineering. |
| 650 24 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Health Informatics. |
| 650 24 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Simulation and Modeling. |
| 650 24 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Programming Techniques. |
| 912 ## - | |
| -- | ZDB-2-SCS |
No items available.