000 | 08060nam a2201261 i 4500 | ||
---|---|---|---|
001 | 6381798 | ||
003 | IEEE | ||
005 | 20220712205841.0 | ||
006 | m o d | ||
007 | cr |n||||||||| | ||
008 | 151222s2013 nju ob 001 eng d | ||
020 | _a9780470876183 | ||
020 |
_a9781118459898 _qebook |
||
020 |
_z9781118459867 _qelectronic |
||
020 |
_z1118459865 _qelectronic |
||
020 |
_z111845989X _qelectronic |
||
020 |
_z9781283858885 _qMyiLibrary |
||
020 |
_z1283858886 _qMyiLibrary |
||
024 | 7 |
_a10.1002/9781118459898 _2doi |
|
035 | _a(CaBNVSL)mat06381798 | ||
035 | _a(IDAMS)0b00006481bea019 | ||
040 |
_aCaBNVSL _beng _erda _cCaBNVSL _dCaBNVSL |
||
050 | 4 |
_aQA76.9.F67 _bF654 2012eb |
|
082 | 0 | 4 |
_a004.01/51 _223 |
245 | 0 | 0 |
_aFormal methods for industrial critical systems : _ba survey of applications / _cedited by Stefania Gnesi, Tiziana Margaria. |
264 | 1 |
_aHoboken, New Jersey : _bJohn Wiley and Sons Incorporated, _c[2012] |
|
264 | 2 |
_a[Piscataqay, New Jersey] : _bIEEE Xplore, _c[2013] |
|
300 | _a1 PDF (292 pages). | ||
336 |
_atext _2rdacontent |
||
337 |
_aelectronic _2isbdmedia |
||
338 |
_aonline resource _2rdacarrier |
||
500 | _aIncludes index. | ||
505 | 0 | _aFOREWORD 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 | _a7.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. | |
506 | 1 | _aRestricted to subscribers or individual electronic text purchasers. | |
520 |
_a"Balances leading edge material, established practice, and reviews of historically important contributions"-- _cProvided by publisher. |
||
530 | _aAlso available in print. | ||
538 | _aMode of access: World Wide Web | ||
588 | _aDescription based on PDF viewed 12/22/2015. | ||
650 | 0 |
_aFormal methods (Computer science) _93854 |
|
655 | 0 |
_aElectronic books. _93294 |
|
695 | _aStochastic processes | ||
695 | _aSynchronization | ||
695 | _aSyntactics | ||
695 | _aTelecommunication services | ||
695 | _aTelecommunication standards | ||
695 | _aTesting | ||
695 | _aUsability | ||
695 | _aXML | ||
695 | _aAdaptation models | ||
695 | _aAerospace electronics | ||
695 | _aAir traffic control | ||
695 | _aAircraft | ||
695 | _aAlgebra | ||
695 | _aAnalytical models | ||
695 | _aAutomata | ||
695 | _aBelts | ||
695 | _aBirds | ||
695 | _aBusiness | ||
695 | _aClocks | ||
695 | _aComputer aided software engineering | ||
695 | _aComputer architecture | ||
695 | _aComputer science | ||
695 | _aComputers | ||
695 | _aConcrete | ||
695 | _aControl theory | ||
695 | _aDesign automation | ||
695 | _aEarth | ||
695 | _aEducational institutions | ||
695 | _aEquations | ||
695 | _aExtrapolation | ||
695 | _aGuidelines | ||
695 | _aHardware | ||
695 | _aIndustries | ||
695 | _aInternet | ||
695 | _aLearning automata | ||
695 | _aMaintenance engineering | ||
695 | _aMarket research | ||
695 | _aMars | ||
695 | _aMathematical model | ||
695 | _aMonitoring | ||
695 | _aNASA | ||
695 | _aPeer to peer computing | ||
695 | _aProbabilistic logic | ||
695 | _aProcess control | ||
695 | _aProcurement | ||
695 | _aProgramming | ||
695 | _aProposals | ||
695 | _aProtocols | ||
695 | _aRadiation detectors | ||
695 | _aRail transportation | ||
695 | _aReal-time systems | ||
695 | _aRuntime | ||
695 | _aSafety | ||
695 | _aSections | ||
695 | _aSemantics | ||
695 | _aSoftware | ||
695 | _aSolid modeling | ||
695 | _aSpace exploration | ||
695 | _aSpace vehicles | ||
695 | _aStandards | ||
700 | 1 |
_aGnesi, Stefania, _d1954- _928127 |
|
700 | 1 |
_aMargaria-Steffen, Tiziana, _d1964- _928128 |
|
710 | 2 |
_aIEEE Xplore (Online Service), _edistributor. _928129 |
|
710 | 2 |
_aWiley InterScience (Online service), _epublisher. _96290 |
|
856 | 4 | 2 |
_3Abstract with links to resource _uhttps://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6381798 |
942 | _cEBK | ||
999 |
_c74281 _d74281 |