Formal methods for industrial critical systems : (Record no. 74281)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 08060nam a2201261 i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 6381798 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20220712205841.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 151222s2013 nju ob 001 eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| ISBN | 9780470876183 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| ISBN | 9781118459898 |
| -- | ebook |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | electronic |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | electronic |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | electronic |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | MyiLibrary |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | MyiLibrary |
| 082 04 - CLASSIFICATION NUMBER | |
| Call Number | 004.01/51 |
| 245 00 - TITLE STATEMENT | |
| Title | Formal methods for industrial critical systems : |
| Sub Title | a survey of applications / |
| 300 ## - PHYSICAL DESCRIPTION | |
| Number of Pages | 1 PDF (292 pages). |
| 500 ## - GENERAL NOTE | |
| Remark 1 | Includes index. |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Remark 2 | FOREWORD by Mike Hinchey xiii -- FOREWORD by Alessandro Fantechi and Pedro Merino xv -- PREFACE xvii -- CONTRIBUTORS xix -- PART I INTRODUCTION AND STATE OF THE ART 1 -- 1 FORMAL METHODS: APPLYING {LOGICS IN, THEORETICAL} COMPUTER SCIENCE 3 -- Diego Latella -- 1.1 Introduction and State of the Art 3 -- 1.2 Future Directions 9 -- PART II MODELING PARADIGMS 15 -- 2 A SYNCHRONOUS LANGUAGE AT WORK: THE STORY OF LUSTRE 17 -- Nicolas Halbwachs -- 2.1 Introduction 17 -- 2.2 A Flavor of the Language 18 -- 2.3 The Design and Development of Lustre and Scade 20 -- 2.4 Some Lessons from Industrial Use 25 -- 2.5 And Now . . . 28 -- 3 REQUIREMENTS OF AN INTEGRATED FORMAL METHOD FOR INTELLIGENT SWARMS 33 -- Mike Hinchey, James L. Rash, Christopher A. Rouff, Walt F. Truszkowski, and Amy K.C.S. Vanderbilt -- 3.1 Introduction 33 -- 3.2 Swarm Technologies 35 -- 3.3 NASA FAST Project 39 -- 3.4 Integrated Swarm Formal Method 41 -- 3.5 Conclusion 55 -- PART III TRANSPORTATION SYSTEMS 61 -- 4 SOME TRENDS IN FORMAL METHODS APPLICATIONS TO RAILWAY SIGNALING 63 -- Alessandro Fantechi, Wan Fokkink, and Angelo Morzenti -- 4.1 Introduction 63 -- 4.2 CENELEC Guidelines 65 -- 4.3 Software Procurement in Railway Signaling 66 -- 4.4 A Success Story: The B Method 70 -- 4.5 Classes of Railway Signaling Equipment 71 -- 4.6 Conclusions 80 -- 5 SYMBOLIC MODEL CHECKING FOR AVIONICS 85 -- Radu I. Siminiceanu and Gianfranco Ciardo -- 5.1 Introduction 85 -- 5.2 Application: The Runway Safety Monitor 87 -- 5.3 A Discrete Model of RSM 95 -- 5.4 Discussion 107 -- PART IV TELECOMMUNICATIONS 113 -- 6 APPLYING FORMAL METHODS TO TELECOMMUNICATION SERVICES WITH ACTIVE NETWORKS 115 -- Marƒia del Mar Gallardo, Jes�us Martƒinez, and Pedro Merino -- 6.1 Overview 115 -- 6.2 Active Networks 116 -- 6.3 The Capsule Approach 117 -- 6.4 Previous Approaches on Analyzing Active Networks 118 -- 6.5 Model Checking Active Networks with SPIN 122 -- 6.6 Conclusions 129 -- 7 PRACTICAL APPLICATIONS OF PROBABILISTIC MODEL CHECKING TO COMMUNICATION PROTOCOLS 133 -- Marie Dufl ot, Marta Kwiatkowska, Gethin Norman, David Parker, Sylvain Peyronnet, Claudine Picaronny, and Jeremy Sproston. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Remark 2 | 7.1 Introduction 133 -- 7.2 PTAs 134 -- 7.3 Probabilistic Model Checking 136 -- 7.4 Case Study: CSMA/CD 139 -- 7.5 Discussion and Conclusion 146 -- PART V INTERNET AND ONLINE SERVICES 151 -- 8 DESIGN FOR VERIFIABILITY: THE OCS CASE STUDY 153 -- Johannes Neubauer, Tiziana Margaria, and Bernhard Steffen -- 8.1 Introduction 153 -- 8.2 The User Model 155 -- 8.3 The Models and the Framework 158 -- 8.4 Model Checking 159 -- 8.5 Validating Emerging Global Behavior via Automata Learning 161 -- 8.6 Related Work 170 -- 8.7 Conclusion and Perspectives 173 -- 9 AN APPLICATION OF STOCHASTIC MODEL CHECKING IN THE INDUSTRY: USER-CENTERED MODELING AND ANALYSIS OF COLLABORATION IN THINKTEAM 179 -- Maurice H. ter Beek, Stefania Gnesi, Diego Latella, Mieke Massink, Maurizio Sebastianis, and Gianluca Trentanni -- 9.1 Introduction 179 -- 9.2 thinkteam 182 -- 9.3 Analysis of the thinkteam Log File 184 -- 9.4 thinkteam with Replicated Vaults 189 -- 9.5 Lessons Learned 201 -- 9.6 Conclusions 201 -- PART VI RUNTIME: TESTING AND MODEL LEARNING 205 -- 10 THE TESTING AND TEST CONTROL NOTATION TTCN-3 AND ITS USE 207 -- Ina Schieferdecker and Alain-Georges Vouffo-Feudjio -- 10.1 Introduction 207 -- 10.2 The Concepts of TTCN-3 210 -- 10.3 An Introductory Example 216 -- 10.4 TTCN-3 Semantics and Its Application 219 -- 10.5 A Distributed Test Platform for the TTCN-3 220 -- 10.6 Case Study I: Testing of Open Service Architecture (OSA)/Parlay Services 223 -- 10.7 Case Study II: Testing of IP Multimedia Subsystem (IMS) Equipment 225 -- 10.8 Conclusion 230 -- 11 PRACTICAL ASPECTS OF ACTIVE AUTOMATA LEARNING 235 -- Falk Howar, Maik Merten, Bernhard Steffen, and Tiziana Margaria -- 11.1 Introduction 235 -- 11.2 Regular Extrapolation 239 -- 11.3 Challenges in Regular Extrapolation 244 -- 11.4 Interacting with Real Systems 247 -- 11.5 Membership Queries 250 -- 11.6 Reset 253 -- 11.7 Parameters and Value Domains 256 -- 11.8 The NGLL 260 -- 11.9 Conclusion and Perspectives 263 -- References 264 -- INDEX 269. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc | "Balances leading edge material, established practice, and reviews of historically important contributions"-- |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| Subject | Formal methods (Computer science) |
| 700 1# - AUTHOR 2 | |
| Author 2 | Gnesi, Stefania, |
| 700 1# - AUTHOR 2 | |
| Author 2 | Margaria-Steffen, Tiziana, |
| 856 42 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | https://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6381798 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | eBooks |
| 264 #1 - | |
| -- | Hoboken, New Jersey : |
| -- | John Wiley and Sons Incorporated, |
| -- | [2012] |
| 264 #2 - | |
| -- | [Piscataqay, New Jersey] : |
| -- | IEEE Xplore, |
| -- | [2013] |
| 336 ## - | |
| -- | text |
| -- | rdacontent |
| 337 ## - | |
| -- | electronic |
| -- | isbdmedia |
| 338 ## - | |
| -- | online resource |
| -- | rdacarrier |
| 520 ## - SUMMARY, ETC. | |
| -- | Provided by publisher. |
| 588 ## - | |
| -- | Description based on PDF viewed 12/22/2015. |
| 695 ## - | |
| -- | Stochastic processes |
| 695 ## - | |
| -- | Synchronization |
| 695 ## - | |
| -- | Syntactics |
| 695 ## - | |
| -- | Telecommunication services |
| 695 ## - | |
| -- | Telecommunication standards |
| 695 ## - | |
| -- | Testing |
| 695 ## - | |
| -- | Usability |
| 695 ## - | |
| -- | XML |
| 695 ## - | |
| -- | Adaptation models |
| 695 ## - | |
| -- | Aerospace electronics |
| 695 ## - | |
| -- | Air traffic control |
| 695 ## - | |
| -- | Aircraft |
| 695 ## - | |
| -- | Algebra |
| 695 ## - | |
| -- | Analytical models |
| 695 ## - | |
| -- | Automata |
| 695 ## - | |
| -- | Belts |
| 695 ## - | |
| -- | Birds |
| 695 ## - | |
| -- | Business |
| 695 ## - | |
| -- | Clocks |
| 695 ## - | |
| -- | Computer aided software engineering |
| 695 ## - | |
| -- | Computer architecture |
| 695 ## - | |
| -- | Computer science |
| 695 ## - | |
| -- | Computers |
| 695 ## - | |
| -- | Concrete |
| 695 ## - | |
| -- | Control theory |
| 695 ## - | |
| -- | Design automation |
| 695 ## - | |
| -- | Earth |
| 695 ## - | |
| -- | Educational institutions |
| 695 ## - | |
| -- | Equations |
| 695 ## - | |
| -- | Extrapolation |
| 695 ## - | |
| -- | Guidelines |
| 695 ## - | |
| -- | Hardware |
| 695 ## - | |
| -- | Industries |
| 695 ## - | |
| -- | Internet |
| 695 ## - | |
| -- | Learning automata |
| 695 ## - | |
| -- | Maintenance engineering |
| 695 ## - | |
| -- | Market research |
| 695 ## - | |
| -- | Mars |
| 695 ## - | |
| -- | Mathematical model |
| 695 ## - | |
| -- | Monitoring |
| 695 ## - | |
| -- | NASA |
| 695 ## - | |
| -- | Peer to peer computing |
| 695 ## - | |
| -- | Probabilistic logic |
| 695 ## - | |
| -- | Process control |
| 695 ## - | |
| -- | Procurement |
| 695 ## - | |
| -- | Programming |
| 695 ## - | |
| -- | Proposals |
| 695 ## - | |
| -- | Protocols |
| 695 ## - | |
| -- | Radiation detectors |
| 695 ## - | |
| -- | Rail transportation |
| 695 ## - | |
| -- | Real-time systems |
| 695 ## - | |
| -- | Runtime |
| 695 ## - | |
| -- | Safety |
| 695 ## - | |
| -- | Sections |
| 695 ## - | |
| -- | Semantics |
| 695 ## - | |
| -- | Software |
| 695 ## - | |
| -- | Solid modeling |
| 695 ## - | |
| -- | Space exploration |
| 695 ## - | |
| -- | Space vehicles |
| 695 ## - | |
| -- | Standards |
No items available.