This book constitutes the thoroughly refereed post-conference proceedings of the 13th Brazilian Symposium on Formal Methods, SBMF 2010, held in Natal, Brazil, in November 2010. The 18 revised full papers were carefully reviewed and selected from 55 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains.
Erscheinungsdatum: 23.03.2011

lgli/R:\062020\springer2\10.1007%2F978-3-642-19829-8.pdf

lgrsnf/R:\062020\springer2\10.1007%2F978-3-642-19829-8.pdf

nexusstc/Formal Methods: Foundations and Applications: 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers/198c4eb463919b8445f4f02fbd4f0b6a.pdf

scihub/10.1007/978-3-642-19829-8.pdf

zlib/Computers/Networking/Michael Leuschel, Jens Bendisposto (auth.), Jim Davies, Leila Silva, Adenilso Simao (eds.)/Formal Methods: Foundations and Applications: 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers_5923710.pdf

Jim Davies; Leila Silva; Adenilso Simão; Brazilian Symposium on Formal Methods

Jim Davies; Leila Silva; Adenilso Simao; SpringerLink (Online service)

edited by Jim Davies, Leila Silva, Adenilso Simao

Juliano Iyoda; Leonardo de Moura

Author

Spektrum Akademischer Verlag. in Springer-Verlag GmbH

Steinkopff. in Springer-Verlag GmbH

Lecture Notes in Computer Science -- 6527, Berlin, Heidelberg, Germany, 2011

Lecture notes in computer science, 8195, Berlin, Heidelberg, 2013

Springer Nature, Berlin, Heidelberg, 2011

Germany, Germany

lg2756854

producers:
Acrobat Distiller 8.0.0 (Windows)

{"container_title":"Lecture Notes in Computer Science","edition":"1","isbns":["3642198287","3642198295","9783642198281","9783642198298"],"issns":["0302-9743","1611-3349"],"last_page":291,"publisher":"Springer","series":"Lecture Notes in Computer Science 6527 : Programming and Software Engineering"}

MiU

Subject
Title Page 1
Preface 4
Organization 5
Table of Contents 6
Directed Model Checking for B: An Evaluation and New Techniques 8
Introduction 8
Combining Depth-First and Breadth-First for Improved Model Checking 9
Depth-First versus Breadth-First: An Empirical Evaluation 11
The Models 11
The Results 11
Evaluating Directed Model Checking 13
Future and Related Work and Conclusion 17
References 17
Midlet Navigation Graphs in JML 24
Introduction 24
MIDP Infrastructure 25
Navigation Graphs 27
Navigation Graphs in JML 28
Relevant API Methods 28
Midlet Annotations – The Mobius Case Study 30
Specification and Verification Issues 34
Evaluation and Discussion 36
References 38
Runtime Verification for Generic Classes with CONGU2 40
Introduction 40
Overview of the ConGu Approach 41
Runtime Conformance of Programs against Modules 44
Object Properties Induced by Specifications 44
Checking Object Properties 47
The New ConGu Tool 48
Analysis of Refinement Mappings 49
Bytecode Instrumentation 50
Generation of Property-Monitoring Classes 51
Conclusions 54
References 55
A High-Level Language for Modeling Algorithms and Their Properties 56
Introduction 56
Evaluation of PlusCal 57
Introducing a New Version of PlusCal 59
Structure of an Algorithm 59
PlusCal Statements 62
The PlusCal Compiler 64
Comparison with Lamport's PlusCal 66
Experiments 67
Related Work 68
Conclusion 69
References 70
A Formal Environment Model for Multi-Agent Systems 71
Introduction 71
Environment Model 73
Underlying Elementary π-Calculus Events 73
Operations 74
Environment Structures 75
Semantics 78
Convenience Elements and Operations 81
Composition Operators 81
Core Operations 82
Example 84
Conclusion 84
References 85
A Modal Interface Theory with Data Constraints 87
Introduction 87
Modal I/O-Transition Systems with Data Constraints 89
Refinement of MIODs 94
Composition and Compatibility of MIODs 96
Conclusion 101
References 102
Synchronizing Model and Program Refactoring 103
Introduction 103
Languages 104
Model Refactoring 104
Program Refactoring 105
Synchronization 107
Synchronizers 107
Consistency Relationship 108
Examples of Synchronizers 109
Soundness 112
Discussion 114
Invariants as Basis for Refactoring Automation 114
Quality of Refactorings 115
Consistency and Synchronizers 115
Related Work 116
Conclusions 117
References 117
A Type-Theoretic Framework for Certified Model Transformations 119
Introduction 119
Outline of the Approach 121
The CIC as a Technical Space 122
The Framework at a Glance 122
A Running Example 123
Formalization of Metamodels and Models 124
Translation of the Model Transformation 127
Verification of Properties 131
Conclusions and Further Work 132
References 134
Simulating Truly Concurrent CSP 135
Introduction 135
CSP 136
The Transformation $T$ 138
Assembling the System 139
Properties 141
Examples 145
Choice versus Concurrency 145
One-Place Buffer 146
Dining Philosophers 146
Related and Further Work 146
Conclusion 148
References 149
Statistical Verification of Probabilistic Properties with Unbounded Until 151
Introduction 151
Probabilistic Model Checking 152
Stochastic Processes and Discrete-Time Markov Chains 153
Temporal Stochastic Logic 153
Error Control 154
Sampling-Based Verification of Unbounded Until 155
Sampling-Based Method with Reachability Analysis 157
Sampling-Based Method with Termination Probability 158
Related Work 160
Empirical Evaluation 162
Modified Polling System 162
Tandem Queuing Network 164
Discussion 165
References 165
Reasoning about Assignments in Recursive Data Structures 168
Introduction 168
Preliminaries 169
The Model 170
The Heap 170
Expressions, Statements and Compositions 171
Assignments 172
The Effect of Assignments on Multidot Expressions 173
Looking at the Heap Before the Assignment 174
Looking at the Heap After the Assignment 175
PVS Formalisation 176
Linearised Abstractions 177
Paths 177
Example: Verification of an In-Place List Reversal Algorithm 178
Other Data Structures 179
Evaluation and Future Work 180
Related Work 181
Conclusions 182
References 182
Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned 184
Introduction 184
Background 185
KAOS Method 185
Event-B Method 186
Experience with the Specification of a Localization Software Component 187
Abstract Model 189
First Refinement 189
Second Refinement 192
Third Refinement 194
Synthesis 196
Lessons Learned 197
Related Work 197
Conclusion and Further Work 198
References 199
A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence 201
Introduction 201
Case Study and Notations 203
Case Study 203
Notation B 204
Logs and Claims 205
System Information 205
Logs and Distribution 206
Properties and Claims 207
Log Functions 208
Log Extraction 208
Log Merge 209
Log Analysis 210
Log Analyzer 210
Incremental Analysis 211
Conclusion 213
Related Works 214
Future Work 214
References 214
Formal Development of a Cardiac Pacemaker: From Specification to Code 217
Introduction 217
The Pacemaker 218
Pacemaker in Z 219
Moving into Code 222
From Z to Perfect Developer 223
Analysis of Results 227
Conclusions 229
References 231
A Decision Procedure for Bisimilarity of Generalized Regular Expressions 233
Introduction 233
Regular Expressions for Polynomial Coalgebras 234
An Algebraic View on the Coalgebra of Generalized Regular Expressions 239
A Decision Procedure for Bisimilarity 242
A CIRC-Based Tool 245
Conclusions and Future Work 247
References 248
Normalization of Linear Horn Clauses 249
Introduction 249
Normalization of Finite Sets of Linear Horn Clauses 250
Basics 250
The Normalization Semi-procedure 252
Instantiation 259
An Application: Backward Reachability Analysis for Constrained Dynamic Pushdown Networks 260
Conclusion 263
References 264
A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs 265
Introduction 265
rCOS 267
Language 267
Mechanized Refinement 268
Graph Representation 270
State Graph 270
Graph Implementation 271
Graph Operations 272
Refinement of rCOS Designs 274
Primitive Designs 274
Composite Designs 276
Application 276
Tool Refinement 276
Provided Lemmas 276
Example 277
Conclusion 278
References 279
Automating Refinement of $Circus$ Programs 281
Introduction 281
Preliminaries 283
Mechanisation of $Circus$ 283
ArcAngelC 284
Managing Well-Definedness 284
Reducing Constraints in the Semantic Encoding 285
A Semantic Formalisation of Well-Formedness 286
ExtensionstotheArcAngelC Implementation 288
Extended Refinement Theorems 288
Structural Combinators 290
Practical Experiences 293
Conclusions 295
References 296
Author Index 298

Front Matter....Pages -
Directed Model Checking for B: An Evaluation and New Techniques....Pages 1-16
Midlet Navigation Graphs in JML....Pages 17-32
Runtime Verification for Generic Classes with ConGu 2....Pages 33-48
A High-Level Language for Modeling Algorithms and Their Properties....Pages 49-63
A Formal Environment Model for Multi-Agent Systems....Pages 64-79
A Modal Interface Theory with Data Constraints....Pages 80-95
Synchronizing Model and Program Refactoring....Pages 96-111
A Type-Theoretic Framework for Certified Model Transformations....Pages 112-127
Simulating Truly Concurrent CSP....Pages 128-143
Statistical Verification of Probabilistic Properties with Unbounded Until....Pages 144-160
Reasoning about Assignments in Recursive Data Structures....Pages 161-176
Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned....Pages 177-193
A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence....Pages 194-209
Formal Development of a Cardiac Pacemaker: From Specification to Code....Pages 210-225
A Decision Procedure for Bisimilarity of Generalized Regular Expressions....Pages 226-241
Normalization of Linear Horn Clauses....Pages 242-257
A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs....Pages 258-273
Automating Refinement of Circus Programs....Pages 274-290
Back Matter....Pages -

This book constitutes the refereed proceedings of the 16th Brazilian Symposium on Formal Methods, SBMF 2013, held in Brasilia, Brazil, in September/October 2013. The 14 revised full papers presented together with 2 keynotes were carefully reviewed and selected from 29 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains

Annotation This book constitutes the thoroughly refereed post-conferenceproceedings of the 13th Brazilian Symposium on Formal Methods, SBMF2010, held in Natal, Brazil, in November 2010. The 18 revised full papers were carefully reviewed and selected from55 submissions. The papers presented cover a broad range of foundationaland methodological issues in formal methods for the design and analysisof software and hardware systems as well as applications in variousdomains

2020-08-30