top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
2013 International Symposium on Theoretical Aspects of Software Engineering : 1-3 July 2013, Birmingham, United Kingdom / / IEEE Computer Society
2013 International Symposium on Theoretical Aspects of Software Engineering : 1-3 July 2013, Birmingham, United Kingdom / / IEEE Computer Society
Pubbl/distr/stampa Piscataway, New Jersey : , : Institute of Electrical and Electronics Engineers, , 2013
Descrizione fisica 1 online resource (128 pages)
Disciplina 005.1
Altri autori (Persone) Margaria-SteffenTiziana <1964->
Soggetto topico Software engineering
Computer software - Development
ISBN 0-7695-5053-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNINA-9910132357503321
Piscataway, New Jersey : , : Institute of Electrical and Electronics Engineers, , 2013
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
2013 International Symposium on Theoretical Aspects of Software Engineering : 1-3 July 2013, Birmingham, United Kingdom / / IEEE Computer Society
2013 International Symposium on Theoretical Aspects of Software Engineering : 1-3 July 2013, Birmingham, United Kingdom / / IEEE Computer Society
Pubbl/distr/stampa Piscataway, New Jersey : , : Institute of Electrical and Electronics Engineers, , 2013
Descrizione fisica 1 online resource (128 pages)
Disciplina 005.1
Altri autori (Persone) Margaria-SteffenTiziana <1964->
Soggetto topico Software engineering
Computer software - Development
ISBN 0-7695-5053-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISA-996280212503316
Piscataway, New Jersey : , : Institute of Electrical and Electronics Engineers, , 2013
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Pubbl/distr/stampa Hoboken, N.J., : John Wiley & Sons Inc., c2013
Descrizione fisica 1 online resource (294 p.)
Disciplina 004.21
620.86028551
Altri autori (Persone) GnesiStefania <1954->
Margaria-SteffenTiziana <1964->
Soggetto topico Formal methods (Computer science)
System design
ISBN 1-118-45989-X
1-283-85888-6
1-118-45986-5
Classificazione COM059000
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto 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ús 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.
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.
Record Nr. UNINA-9910877377103321
Hoboken, N.J., : John Wiley & Sons Inc., c2013
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Pubbl/distr/stampa Hoboken, New Jersey : , : John Wiley and Sons Incorporated, , [2012]
Descrizione fisica 1 online resource (294 p.)
Disciplina 004.21
620.86028551
Altri autori (Persone) GnesiStefania <1954->
Margaria-SteffenTiziana <1964->
Soggetto topico Formal methods (Computer science)
System design
ISBN 1-118-45989-X
1-283-85888-6
1-118-45986-5
Classificazione COM059000
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto 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ús 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.
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.
Record Nr. UNINA-9910141360103321
Hoboken, New Jersey : , : John Wiley and Sons Incorporated, , [2012]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Pubbl/distr/stampa Hoboken, New Jersey : , : John Wiley and Sons Incorporated, , [2012]
Descrizione fisica 1 online resource (294 p.)
Disciplina 004.21
620.86028551
Altri autori (Persone) GnesiStefania <1954->
Margaria-SteffenTiziana <1964->
Soggetto topico Formal methods (Computer science)
System design
ISBN 1-118-45989-X
1-283-85888-6
1-118-45986-5
Classificazione COM059000
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto 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ús 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.
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.
Record Nr. UNINA-9910830558103321
Hoboken, New Jersey : , : John Wiley and Sons Incorporated, , [2012]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering : proceedings, Beijing, China, 4-6 July 2012 / / edited by Tiziana Margaria, Zongyan Qiu and Hongli Yang ; sponsored by IEEE Computer Society, IFIP [and] Beijing University of Technology
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering : proceedings, Beijing, China, 4-6 July 2012 / / edited by Tiziana Margaria, Zongyan Qiu and Hongli Yang ; sponsored by IEEE Computer Society, IFIP [and] Beijing University of Technology
Descrizione fisica x, 284 p. : ill. ; ; 28 cm
Disciplina 005.1
Altri autori (Persone) Margaria-SteffenTiziana <1964->
QiuZongyan
YangHongli, program co-chair
Soggetto topico Software engineering
Computer software - Development
Soggetto genere / forma Conference proceedings.
ISBN 0-7695-4751-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Sixth International Symposium on Theoretical Aspects of Software Engineering
Theoretical aspects of software engineering
2012 IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering
TASE 2012
2012 Sixth International Conference on Theoretical Aspects of Software Engineering
Record Nr. UNISA-996200470703316
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering : proceedings, Beijing, China, 4-6 July 2012 / / edited by Tiziana Margaria, Zongyan Qiu and Hongli Yang ; sponsored by IEEE Computer Society, IFIP [and] Beijing University of Technology
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering : proceedings, Beijing, China, 4-6 July 2012 / / edited by Tiziana Margaria, Zongyan Qiu and Hongli Yang ; sponsored by IEEE Computer Society, IFIP [and] Beijing University of Technology
Descrizione fisica x, 284 p. : ill. ; ; 28 cm
Disciplina 005.1
Altri autori (Persone) Margaria-SteffenTiziana <1964->
QiuZongyan
YangHongli, program co-chair
Soggetto topico Software engineering
Computer software - Development
Soggetto genere / forma Conference proceedings.
ISBN 0-7695-4751-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Sixth International Symposium on Theoretical Aspects of Software Engineering
Theoretical aspects of software engineering
2012 IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering
TASE 2012
2012 Sixth International Conference on Theoretical Aspects of Software Engineering
Record Nr. UNINA-9910619131103321
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Leveraging applications of formal methods : first international symposium, ISoLA 2004, Paphos, Cyprus, October 30-November 2, 2004 : revised selected papers / / Tiziana Margaria, Bernhard Steffen (eds.)
Leveraging applications of formal methods : first international symposium, ISoLA 2004, Paphos, Cyprus, October 30-November 2, 2004 : revised selected papers / / Tiziana Margaria, Bernhard Steffen (eds.)
Edizione [1st ed. 2006.]
Pubbl/distr/stampa Berlin ; ; New York, : Springer, c2006
Descrizione fisica 1 online resource (VI, 197 p.)
Disciplina 005.1
Altri autori (Persone) Margaria-SteffenTiziana <1964->
SteffenBernhard
Collana Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues
Soggetto topico Formal methods (Computer science)
ISBN 3-540-48929-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Interaction and Coordination of Tools for Structured Data -- Modelling Coordination in Biological Systems -- A Rule Markup Language and Its Application to UML -- Using XML Transformations for Enterprise Architectures -- Classification and Utilization of Abstractions for Optimization -- On the Correctness of Transformations in Compiler Back-Ends -- Accurate Theorem Proving for Program Verification -- Designing Safe, Reliable Systems Using Scade -- Decreasing Maintenance Costs by Introducing Formal Analysis of Real-Time Behavior in Industrial Settings -- Static Timing Analysis of Real-Time Operating System Code -- A Case Study in Domain-Customized Model Checking for Real-Time Component Software -- Models for Contract Conformance.
Altri titoli varianti ISoLA 2004
Record Nr. UNINA-9910484570103321
Berlin ; ; New York, : Springer, c2006
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors)
Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (608 pages)
Disciplina 006.3
Collana Lecture notes in computer science
Soggetto topico Artificial intelligence
Data mining
Electronic data processing
ISBN 3-031-19849-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Introduction -- Organization -- Contents - Part I -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- 1 Introduction -- 2 Summary of Contributions -- References -- Deductive Verification Based Abstraction for Software Model Checking -- 1 Introduction -- 2 Overview of the Verification Approach -- 3 Deductive Verification and Frama-C -- 4 Model Checking and TLA -- 4.1 The TLA Framework -- 4.2 Translating Code and Contracts into TLA -- 5 Contracts as a Unifying Theory -- 5.1 An Abstract Contract Theory -- 5.2 Deductive Verification in the Abstract Contract Theory -- 5.3 Procedure-Modular Verification with TLA -- 5.4 Contract Based System Design -- 6 Preliminary Evaluation -- 6.1 Simple File Open-Close Example -- 6.2 Simplified Industrial Example -- 7 Conclusion -- References -- Abstraction in Deductive Verification: Model Fields and Model Methods -- 1 Introduction -- 2 Logical Encoding of Local Computations -- 3 Encoding Heap Access and Update-Previous and Related Work -- 3.1 Notation -- 3.2 Heaps as Maps -- 3.3 Arrays -- 3.4 Embedding in SMT -- 4 Model Fields and Model Methods -- 5 Simple Example -- 6 Using Model Methods -- 7 Encoding Model Methods -- 8 Contrast and Conclusion -- References -- A Hoare Logic with Regular Behavioral Specifications -- 1 Introduction -- 2 Motivation -- 3 Approach -- 3.1 Preliminaries and Notation -- 3.2 Regular Behavioral Specifications -- 3.3 Programs and Behavioral Correctness -- 3.4 Hoare Logic Proof Rules -- 4 Tool Support in SecC -- 4.1 Specification Syntax -- 4.2 Verification Engine -- 5 Case Studies -- 5.1 Case Study: Regular Expression Matching -- 5.2 Case-Study: VerifyThis Casino Challenge -- 5.3 Discussion -- 6 Related and Alternative Approaches -- 7 Conclusion -- References.
Specification-Based Monitoring in C++ -- 1 Introduction -- 2 Related Work -- 3 Overview -- 4 The Specification Language -- 4.1 Events -- 4.2 A Simple State Machine -- 4.3 Some Alternative Monitors -- 4.4 Monitoring Events that Carry Data -- 4.5 Referring to the Past -- 4.6 A Complex Property -- 4.7 The Complete Grammar -- 5 Usage -- 6 Implementation -- 7 Experiment -- 7.1 Setting Up the Experiment -- 7.2 Result and Interpretation -- 8 Conclusion -- A Visualization of Monitors -- References -- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS -- 1 Introduction -- 2 Specifying Termination Detection -- 3 Verification by Model Checking and Theorem Proving -- 3.1 Finite-State Model Checking Using tlc -- 3.2 Bounded Model Checking with Apalache -- 3.3 Theorem Proving Using tlaps -- 4 Safra's Algorithm for Termination Detection -- 5 Analyzing Safra's Algorithm -- 5.1 Model Checking Correctness Properties -- 5.2 Safra's Algorithm Implements Termination Detection -- 5.3 Proving Correctness Using tlaps -- 6 Conclusion -- References -- Selective Presumed Benevolence in Multi-party System Verification -- 1 Introduction -- 2 Smart Contracts, Solidity and Reentrancy -- 3 Semantics of Solidity and Handling of Callbacks -- 4 Presumption of Benevolence -- 4.1 Presuming Benevolence of Oneself -- 4.2 Presuming Benevolence of a Static Group -- 4.3 Presuming Benevolence of a Dynamic Group -- 5 Collaborative Malicious Behaviour -- 6 Conclusions -- References -- On the Pragmatics of Moving from System Models to Program Contracts -- 1 Introduction -- 2 The PGP Server Hagrid -- 3 The Alloy Model -- 4 From Alloy to VCC Contracts -- 4.1 Precondition and Framing Analysis -- 4.2 Translation to Annotated C -- 4.3 Contract Augmentation -- 5 Discussion -- References -- X-by-Construction Meets Runtime Verification.
X-by-Construction Meets Runtime Verification -- 1 Motivation -- 2 Aim -- 3 Contributions -- 3.1 CbC: Robustness, Co-piloting, and Digital Twinning -- 3.2 CbC and RV: Configurable and Cyber-Physical Systems -- 3.3 XbC: Security, Resilience, and Consumption Properties -- 3.4 CbC and RV: Reinforcement Learning and Synthesis -- References -- Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime -- 1 Introduction -- 2 Preliminaries -- 3 Adaptive Strategies -- 3.1 Definitions -- 3.2 Computing Adaptive Strategies -- 4 Strongly Adaptive Strategies -- 4.1 Bad Moves -- 4.2 Motivating Example -- 4.3 Definitions -- 4.4 Existence of Strongly Adaptive Strategies -- 4.5 Computing Strongly Adaptive Strategies -- 5 Conclusion -- References -- TriCo-Triple Co-piloting of Implementation, Specification and Tests -- 1 Introduction -- 1.1 Triple Co-piloting at a Glance -- 2 Emerging Trends in Software Technology -- 2.1 Code Synthesis Through Large Language Models -- 2.2 Automated Test Case Generation -- 2.3 Specification Synthesis -- 2.4 Formal Software Verification -- 3 The TriCo Methodology -- 3.1 Envisaged Workflow -- 3.2 Use Cases -- 3.3 Envisaged Technology -- 4 Research Efforts Required for TriCo -- 5 Turning Vision into Reality -- References -- Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins -- 1 Introduction -- 2 Twinned-by-Construction Systems -- 3 Twinning-by-Construction and Temporal Properties -- 4 The Digital Thread as a Temporal Property -- 5 Related Work -- 6 Conclusion -- References -- On Formal Choreographic Modelling: A Case Study in EU Business Processes -- 1 Introduction -- 2 Background -- 3 Legal Provisions -- 4 Formal Models -- 5 From BPMN to Global Choreographies -- 6 Conclusions and Future Work -- References -- Configurable-by-Construction Runtime Monitoring -- 1 Introduction.
2 The Quest of Configurable Runtime Monitoring -- 2.1 Feature-Oriented Example -- 2.2 Challenges -- 2.3 This Paper -- 3 Configurable Automata-Based Monitoring -- 3.1 Preliminaries -- 3.2 Featured Monitors -- 3.3 Synthesizing Featured Monitors -- 3.4 Concise Featured Monitors -- 4 Configurable Stream-Based Monitoring -- 4.1 Preliminaries -- 4.2 Configurable Lola -- 4.3 Family-Based Specification Analysis -- 5 Concluding Remarks -- References -- Runtime Verification of Correct-by-Construction Driving Maneuvers -- 1 Introduction -- 2 Workflow by Example -- 3 Modeling and Verifying Maneuvers with Hybrid Mode Automata -- 3.1 Formalization of Hybrid Mode Automata -- 3.2 Verification Based on Differential Dynamic Logic -- 4 Runtime Verification of HMA Models -- 4.1 Generating Monitor Conditions for Runtime Verification -- 4.2 Simulation -- 5 Evaluation -- 5.1 Case Studies and Setup -- 5.2 Results and Insights -- 6 Related Work -- 7 Conclusion -- References -- Leveraging System Dynamics in Runtime Verification of Cyber-Physical Systems -- 1 Introduction -- 2 Preliminary Concepts -- 2.1 Signal Model -- 2.2 Signal Temporal Logic (STL) ch16mn04 -- 3 Exploiting Knowledge of System Dynamics -- 3.1 Motivating Example -- 3.2 System Model -- 3.3 Knowledge of Signal Dynamics -- 3.4 Using Partial Knowledge -- 4 Monitoring Distributed CPS -- 4.1 Distributed CPS Architecture -- 4.2 Additional Challenges in the Distributed Setup -- 5 Using Verified Dynamics -- 6 Conclusion -- References -- Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept -- 1 Introduction -- 2 Background and Related Work -- 2.1 Essentials of Statistical Model Checking -- 2.2 Trace Execution Properties -- 2.3 Probabilistic Verification -- 2.4 SMC Tools -- 3 Illustrative Example -- 3.1 SMC-Based Validation -- 3.2 Using Traces for Automated Program Repair.
4 Designing a Repair Agent -- 4.1 A SMC-Based Program Repair Algorithm -- 5 Implementation and Experimental Results -- 5.1 Experimental Results -- 6 Conclusions and Future Work -- References -- Towards Safe and Resilient Hybrid Systems in the Presence of Learning and Uncertainty -- 1 Introduction -- 2 Background -- 2.1 Reinforcement Learning (RL) -- 2.2 Simulink and the RL Toolbox -- 2.3 Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 2.5 Stochastic Hybrid Model -- 2.6 Signal Temporal Logic -- 2.7 Learning Optimal Decisions for Stochastic Hybrid Systems -- 3 Related Work -- 4 Combining Deductive and Quantitative Analyses -- 4.1 An Intelligent Water Distribution System -- 4.2 Formal Verification of Safety and Resilience -- 4.3 Resilient Scheduling Under Uncertainty -- 5 Evaluation -- 5.1 Deductive Verification -- 5.2 Quantitative Analysis -- 6 Conclusion -- References -- Non-functional Testing of Runtime Enforcers in Android -- 1 Introduction -- 2 Background -- 2.1 Runtime Policy -- 2.2 Policy Enforcement Models -- 3 Test4Enforcers -- 3.1 Test Case Generation -- 3.2 Test Execution -- 4 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Automata Learning Meets Shielding -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Markov Decision Processes and Reinforcement Learning -- 3.2 Learning of MDPs -- 3.3 Shielding in MDPs -- 4 Learned Shields for Safe RL -- 4.1 Setting and Problem Statement -- 4.2 Overview of Iterative Safe RL via Learned Shields -- 4.3 Details for Training Using Learned Shields -- 5 Experiments -- 5.1 Case Study Subjects -- 5.2 Experimental Results -- 5.3 Zigzag Gridworlds -- 5.4 Slippery Shortcuts Gridworlds -- 5.5 Wall Gridworlds -- 5.6 Discussion -- 6 Conclusion -- References -- Safe Policy Improvement in Constrained Markov Decision Processes -- 1 Introduction.
2 Motivating Example.
Record Nr. UNINA-9910619268603321
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors)
Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (608 pages)
Disciplina 006.3
Collana Lecture notes in computer science
Soggetto topico Artificial intelligence
Data mining
Electronic data processing
ISBN 3-031-19849-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Introduction -- Organization -- Contents - Part I -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- 1 Introduction -- 2 Summary of Contributions -- References -- Deductive Verification Based Abstraction for Software Model Checking -- 1 Introduction -- 2 Overview of the Verification Approach -- 3 Deductive Verification and Frama-C -- 4 Model Checking and TLA -- 4.1 The TLA Framework -- 4.2 Translating Code and Contracts into TLA -- 5 Contracts as a Unifying Theory -- 5.1 An Abstract Contract Theory -- 5.2 Deductive Verification in the Abstract Contract Theory -- 5.3 Procedure-Modular Verification with TLA -- 5.4 Contract Based System Design -- 6 Preliminary Evaluation -- 6.1 Simple File Open-Close Example -- 6.2 Simplified Industrial Example -- 7 Conclusion -- References -- Abstraction in Deductive Verification: Model Fields and Model Methods -- 1 Introduction -- 2 Logical Encoding of Local Computations -- 3 Encoding Heap Access and Update-Previous and Related Work -- 3.1 Notation -- 3.2 Heaps as Maps -- 3.3 Arrays -- 3.4 Embedding in SMT -- 4 Model Fields and Model Methods -- 5 Simple Example -- 6 Using Model Methods -- 7 Encoding Model Methods -- 8 Contrast and Conclusion -- References -- A Hoare Logic with Regular Behavioral Specifications -- 1 Introduction -- 2 Motivation -- 3 Approach -- 3.1 Preliminaries and Notation -- 3.2 Regular Behavioral Specifications -- 3.3 Programs and Behavioral Correctness -- 3.4 Hoare Logic Proof Rules -- 4 Tool Support in SecC -- 4.1 Specification Syntax -- 4.2 Verification Engine -- 5 Case Studies -- 5.1 Case Study: Regular Expression Matching -- 5.2 Case-Study: VerifyThis Casino Challenge -- 5.3 Discussion -- 6 Related and Alternative Approaches -- 7 Conclusion -- References.
Specification-Based Monitoring in C++ -- 1 Introduction -- 2 Related Work -- 3 Overview -- 4 The Specification Language -- 4.1 Events -- 4.2 A Simple State Machine -- 4.3 Some Alternative Monitors -- 4.4 Monitoring Events that Carry Data -- 4.5 Referring to the Past -- 4.6 A Complex Property -- 4.7 The Complete Grammar -- 5 Usage -- 6 Implementation -- 7 Experiment -- 7.1 Setting Up the Experiment -- 7.2 Result and Interpretation -- 8 Conclusion -- A Visualization of Monitors -- References -- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS -- 1 Introduction -- 2 Specifying Termination Detection -- 3 Verification by Model Checking and Theorem Proving -- 3.1 Finite-State Model Checking Using tlc -- 3.2 Bounded Model Checking with Apalache -- 3.3 Theorem Proving Using tlaps -- 4 Safra's Algorithm for Termination Detection -- 5 Analyzing Safra's Algorithm -- 5.1 Model Checking Correctness Properties -- 5.2 Safra's Algorithm Implements Termination Detection -- 5.3 Proving Correctness Using tlaps -- 6 Conclusion -- References -- Selective Presumed Benevolence in Multi-party System Verification -- 1 Introduction -- 2 Smart Contracts, Solidity and Reentrancy -- 3 Semantics of Solidity and Handling of Callbacks -- 4 Presumption of Benevolence -- 4.1 Presuming Benevolence of Oneself -- 4.2 Presuming Benevolence of a Static Group -- 4.3 Presuming Benevolence of a Dynamic Group -- 5 Collaborative Malicious Behaviour -- 6 Conclusions -- References -- On the Pragmatics of Moving from System Models to Program Contracts -- 1 Introduction -- 2 The PGP Server Hagrid -- 3 The Alloy Model -- 4 From Alloy to VCC Contracts -- 4.1 Precondition and Framing Analysis -- 4.2 Translation to Annotated C -- 4.3 Contract Augmentation -- 5 Discussion -- References -- X-by-Construction Meets Runtime Verification.
X-by-Construction Meets Runtime Verification -- 1 Motivation -- 2 Aim -- 3 Contributions -- 3.1 CbC: Robustness, Co-piloting, and Digital Twinning -- 3.2 CbC and RV: Configurable and Cyber-Physical Systems -- 3.3 XbC: Security, Resilience, and Consumption Properties -- 3.4 CbC and RV: Reinforcement Learning and Synthesis -- References -- Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime -- 1 Introduction -- 2 Preliminaries -- 3 Adaptive Strategies -- 3.1 Definitions -- 3.2 Computing Adaptive Strategies -- 4 Strongly Adaptive Strategies -- 4.1 Bad Moves -- 4.2 Motivating Example -- 4.3 Definitions -- 4.4 Existence of Strongly Adaptive Strategies -- 4.5 Computing Strongly Adaptive Strategies -- 5 Conclusion -- References -- TriCo-Triple Co-piloting of Implementation, Specification and Tests -- 1 Introduction -- 1.1 Triple Co-piloting at a Glance -- 2 Emerging Trends in Software Technology -- 2.1 Code Synthesis Through Large Language Models -- 2.2 Automated Test Case Generation -- 2.3 Specification Synthesis -- 2.4 Formal Software Verification -- 3 The TriCo Methodology -- 3.1 Envisaged Workflow -- 3.2 Use Cases -- 3.3 Envisaged Technology -- 4 Research Efforts Required for TriCo -- 5 Turning Vision into Reality -- References -- Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins -- 1 Introduction -- 2 Twinned-by-Construction Systems -- 3 Twinning-by-Construction and Temporal Properties -- 4 The Digital Thread as a Temporal Property -- 5 Related Work -- 6 Conclusion -- References -- On Formal Choreographic Modelling: A Case Study in EU Business Processes -- 1 Introduction -- 2 Background -- 3 Legal Provisions -- 4 Formal Models -- 5 From BPMN to Global Choreographies -- 6 Conclusions and Future Work -- References -- Configurable-by-Construction Runtime Monitoring -- 1 Introduction.
2 The Quest of Configurable Runtime Monitoring -- 2.1 Feature-Oriented Example -- 2.2 Challenges -- 2.3 This Paper -- 3 Configurable Automata-Based Monitoring -- 3.1 Preliminaries -- 3.2 Featured Monitors -- 3.3 Synthesizing Featured Monitors -- 3.4 Concise Featured Monitors -- 4 Configurable Stream-Based Monitoring -- 4.1 Preliminaries -- 4.2 Configurable Lola -- 4.3 Family-Based Specification Analysis -- 5 Concluding Remarks -- References -- Runtime Verification of Correct-by-Construction Driving Maneuvers -- 1 Introduction -- 2 Workflow by Example -- 3 Modeling and Verifying Maneuvers with Hybrid Mode Automata -- 3.1 Formalization of Hybrid Mode Automata -- 3.2 Verification Based on Differential Dynamic Logic -- 4 Runtime Verification of HMA Models -- 4.1 Generating Monitor Conditions for Runtime Verification -- 4.2 Simulation -- 5 Evaluation -- 5.1 Case Studies and Setup -- 5.2 Results and Insights -- 6 Related Work -- 7 Conclusion -- References -- Leveraging System Dynamics in Runtime Verification of Cyber-Physical Systems -- 1 Introduction -- 2 Preliminary Concepts -- 2.1 Signal Model -- 2.2 Signal Temporal Logic (STL) ch16mn04 -- 3 Exploiting Knowledge of System Dynamics -- 3.1 Motivating Example -- 3.2 System Model -- 3.3 Knowledge of Signal Dynamics -- 3.4 Using Partial Knowledge -- 4 Monitoring Distributed CPS -- 4.1 Distributed CPS Architecture -- 4.2 Additional Challenges in the Distributed Setup -- 5 Using Verified Dynamics -- 6 Conclusion -- References -- Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept -- 1 Introduction -- 2 Background and Related Work -- 2.1 Essentials of Statistical Model Checking -- 2.2 Trace Execution Properties -- 2.3 Probabilistic Verification -- 2.4 SMC Tools -- 3 Illustrative Example -- 3.1 SMC-Based Validation -- 3.2 Using Traces for Automated Program Repair.
4 Designing a Repair Agent -- 4.1 A SMC-Based Program Repair Algorithm -- 5 Implementation and Experimental Results -- 5.1 Experimental Results -- 6 Conclusions and Future Work -- References -- Towards Safe and Resilient Hybrid Systems in the Presence of Learning and Uncertainty -- 1 Introduction -- 2 Background -- 2.1 Reinforcement Learning (RL) -- 2.2 Simulink and the RL Toolbox -- 2.3 Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 2.5 Stochastic Hybrid Model -- 2.6 Signal Temporal Logic -- 2.7 Learning Optimal Decisions for Stochastic Hybrid Systems -- 3 Related Work -- 4 Combining Deductive and Quantitative Analyses -- 4.1 An Intelligent Water Distribution System -- 4.2 Formal Verification of Safety and Resilience -- 4.3 Resilient Scheduling Under Uncertainty -- 5 Evaluation -- 5.1 Deductive Verification -- 5.2 Quantitative Analysis -- 6 Conclusion -- References -- Non-functional Testing of Runtime Enforcers in Android -- 1 Introduction -- 2 Background -- 2.1 Runtime Policy -- 2.2 Policy Enforcement Models -- 3 Test4Enforcers -- 3.1 Test Case Generation -- 3.2 Test Execution -- 4 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Automata Learning Meets Shielding -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Markov Decision Processes and Reinforcement Learning -- 3.2 Learning of MDPs -- 3.3 Shielding in MDPs -- 4 Learned Shields for Safe RL -- 4.1 Setting and Problem Statement -- 4.2 Overview of Iterative Safe RL via Learned Shields -- 4.3 Details for Training Using Learned Shields -- 5 Experiments -- 5.1 Case Study Subjects -- 5.2 Experimental Results -- 5.3 Zigzag Gridworlds -- 5.4 Slippery Shortcuts Gridworlds -- 5.5 Wall Gridworlds -- 5.6 Discussion -- 6 Conclusion -- References -- Safe Policy Improvement in Constrained Markov Decision Processes -- 1 Introduction.
2 Motivating Example.
Record Nr. UNISA-996495569403316
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui