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.