Abstract State Machines, Alloy, B and Z: Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings

Abstract State Machines, Alloy, B and Z: Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings

Description

This book constitutes the proceedings of the Second International Conference on Abstract State Machines, B and Z, which took place in Orford, QC, Canada, in February 2010. The 26 full papers presented were carefully reviewed and selected from 60 submissions. The book also contains two invited talks and abstracts of 18 short papers which address work in progress, industrial experience reports and tool descriptions. The papers cover recent advances in four equally rigorous methods for software and hardware development: abstract state machines (ASM), Alloy, B and Z. They share a common conceptual framework, centered around the notions of state and operation, and promote mathematical precision in the modeling, verification and construction of highly dependable systems.

Table of contents

3642118100......Page 1
Lecture Notes in Computer Science 5977......Page 2
Preface......Page 5
Table of Contents......Page 10
A Structure for Dependability Arguments......Page 14
Introduction......Page 15
Formal Probabilistic Analysis Framework......Page 17
Discrete Random Variables and the PMF......Page 18
Continuous Random Variables and the CDF......Page 19
Statistical Properties for Discrete Random Variables......Page 20
Statistical Properties for Continuous Random Variables......Page 22
Probabilistic Analysis of the Coupon Collector`s Problem......Page 23
Performance Analysis of the Stop-and-Wait Protocol......Page 24
Reliability Analysis of Reconfigurable Memory Arrays......Page 26
Round-Off Error Analysis in Floating-Point Representation......Page 27
Related Work......Page 28
Conclusions......Page 30
References......Page 31
Introduction......Page 33
Scheduling......Page 34
The MsgPassCtl Machine (Ground Model)......Page 36
Properties of MsgPassCtl Runs......Page 38
Semaphores......Page 40
The MsgPassSema Machine......Page 42
Correctness Proof for MsgPassSema......Page 43
Equivalence Proof......Page 44
Concluding Remarks and Future Work......Page 45
References......Page 46
Introduction......Page 47
Related Work......Page 48
Selected Time Criteria......Page 49
A Basic Timed UCM Example......Page 50
Timed UCM Simulation Engine......Page 51
Interleaving Semantics......Page 52
True Concurrency Semantics......Page 54
Multi-Agent Solution: Run to Completion......Page 55
Illustrative Example......Page 56
Conclusions......Page 58
References......Page 59
Introduction......Page 60
Requirements and Design Decisions......Page 61
Extending CoreASM......Page 62
3.1 Extending the Control Flow of the Engine......Page 63
3.2 Extending the Parser......Page 65
Case Study......Page 66
Related Work......Page 70
Conclusion and Future Work......Page 72
References......Page 73
Introduction......Page 74
Related Work......Page 75
ASMETA Toolset......Page 76
NuSMV......Page 77
AsmetaSMV......Page 78
Mapping of States......Page 79
Mapping of Transition Rules......Page 81
Property Specification......Page 82
Property Verification......Page 83
Case Studies......Page 85
References......Page 86
Introduction......Page 88
The SystemC UML Profile......Page 89
ASM-Based Semantic Framework......Page 91
Meta-hooking for the SystemC Process State Machines......Page 93
ASM Signature......Page 95
ASM Transition System......Page 98
ASM Initial State......Page 100
Related Work......Page 101
References......Page 102
Introduction......Page 104
The FracToy Methodology......Page 105
The ``Room`` Scenario......Page 107
Specification of the Component Model......Page 108
Specification of the Self-configurable Room System......Page 112
Analysis of the Room Architecture......Page 114
Related Work......Page 115
References......Page 116
Introduction......Page 118
Encoding......Page 119
Very Simple Vending Machines......Page 120
More Complex Vending Machines......Page 122
Model......Page 124
The Transmitter/Receiver Pair Is a Protocol......Page 126
The Triple-Redundancy Protocol Connected via a Good Network......Page 127
The Triple-Redundancy Protocol Connected via a Bad Network......Page 128
Conclusions......Page 129
References......Page 130
Introduction......Page 131
Alloy and Dynamic Systems......Page 132
Dynamic Fields......Page 133
Action Language......Page 134
River Crossing......Page 135
Filesystem......Page 136
Insertion Sort......Page 138
Translation to Alloy......Page 139
Translation......Page 141
Related Work......Page 142
References......Page 143
Introduction......Page 145
Architectural Styles: What and Why?......Page 146
Alloy......Page 147
Case Study......Page 149
FARA Model......Page 150
Related Work......Page 156
Discussion, Future Work, and Conclusion......Page 157
References......Page 158
Background......Page 159
Design......Page 161
Model Template......Page 164
Class2Alloy Classfile Parser......Page 169
Analysis of the BlackBox Applet......Page 170
Conclusion......Page 171
References......Page 172
Introduction......Page 173
Motivation......Page 174
Finding Minimal Sets of Hot Clauses......Page 178
Overview of the SAT-Solving Process......Page 179
Activity Heuristics in the Search Process......Page 180
Extracting the Core......Page 181
Experimental Results......Page 182
Conclusions and Further Work......Page 185
References......Page 186
Introduction......Page 187
Challenges and Experiences in Formal Development of Onboard Software......Page 188
Event B......Page 189
Introduction to Modules in Event B......Page 190
Introducing Modules via Model Decomposition......Page 191
System Development via Model Composition......Page 192
Extending Event B with Modules......Page 194
Module Body......Page 195
Operation Invocation......Page 196
Modularisation of the DPU Unit......Page 197
Conclusions......Page 199
References......Page 200
Introduction......Page 202
Background......Page 203
From Proof Critics to Reasoned Modelling Critics......Page 204
Guidance for Invariant Proof Failures via Local Analysis......Page 206
The Cruise Control System in Event-B......Page 209
From Local to Global Modelling Suggestions......Page 212
Related and Future Work......Page 213
Conclusion......Page 214
References......Page 215
Introduction......Page 216
Smart Card System......Page 217
Developing Java Card Applications......Page 218
Formal Java Card Development with the B Method......Page 219
Generation of the Host Application API......Page 220
Rules for Host API Code Generation......Page 222
Development of the Card-Side Application......Page 223
Tool Support......Page 225
A Library of Reusable B Components......Page 226
Conclusions......Page 228
References......Page 229
Introduction......Page 230
Proof Obligations in Rodin......Page 231
The SMT-LIB Format......Page 232
Rationale of the Translation......Page 233
Preliminary Definitions and Notations......Page 235
Translation Rules for the Typing Environment......Page 236
Translation Rules for Formulas......Page 237
Translation Rules for Terms......Page 238
Mixed Operators......Page 239
Experimental Results......Page 240
Conclusions......Page 242
References......Page 243
Introduction......Page 244
An Abstract Specification for Model Checking......Page 245
Refinement Level 1......Page 247
Refinement for Standard Model Checking......Page 249
Level 1......Page 251
Level 2......Page 255
Concluding......Page 256
References......Page 257
Introduction......Page 258
AADL Data Port Protocol......Page 259
Motivation of the Development......Page 260
The Specification View......Page 261
The Operational View......Page 262
Abstracting and Refining the AADL Data Port Protocol......Page 263
The Specification......Page 264
Introducing Idle Ports and Atomicity Breaking through Silent Steps......Page 265
Partitioning the Ports......Page 266
Development Validation......Page 267
Recursive Function Patterns......Page 268
Related Work......Page 269
References......Page 270
Introduction......Page 272
A Formal Framework for Social Networking......Page 273
The B Method for Software Development......Page 274
Matelas......Page 275
Publishing Content......Page 281
Related Work......Page 282
Conclusion......Page 283
References......Page 284
Introduction......Page 286
Notation......Page 287
Proof Obligations......Page 288
Without Structure......Page 290
With Structure......Page 291
Development of a Sequential Program......Page 292
GCD by Way of a Linear Equation......Page 293
Creation of a Stack of Divisions......Page 294
Calculation of the Coefficients......Page 295
Implementation of the Stack Pointer......Page 296
Related and Future Work......Page 297
Conclusion......Page 298
References......Page 299
Introduction and Motivation......Page 300
Contexts......Page 301
Machines......Page 302
Machine Refinement......Page 304
Common Variables and Common Parameters......Page 305
Refined Events and Witnesses......Page 306
New Events and Convergence......Page 307
Preprocessing......Page 308
The Animation Algorithm......Page 309
Detection of Specific Problems......Page 310
Application to Case Studies......Page 311
Related Work......Page 312
References......Page 313
Introduction......Page 315
The Fibonacci Generator......Page 317
The rB Action Notation......Page 319
The Vending Machine......Page 320
The Fuel Pump......Page 321
Unifying Theories of Programming......Page 322
Relational Semantics of Sequential Programs......Page 323
Relational Semantics of Reactive Programs......Page 324
Reactive Healthiness Conditions......Page 325
Semantics of rB Actions......Page 326
The Maritime Port......Page 327
Conclusion and Future Work......Page 329
References......Page 330
Introduction......Page 332
Machines......Page 333
Machine Refinement......Page 334
Shared Variable Decomposition......Page 335
Example: FindP Program......Page 336
Formal Development......Page 337
First Refinement......Page 338
Decomposition......Page 339
Further (sub-)refinements......Page 340
Proof Statistics......Page 342
RelatedWork......Page 343
References......Page 345
Introduction......Page 347
ClawZ......Page 348
Signal-Processing Features......Page 350
Addition of Data Types......Page 351
Support for Communication Blocks......Page 354
Case Study: Software-Defined Radio......Page 357
Conclusion and Future Work......Page 359
References......Page 360
Introduction......Page 362
Formalising RBAC......Page 363
Formalising XACML......Page 364
Helper Functions......Page 368
Translation......Page 369
Towards an Alloy Model for Formal Analysis......Page 371
Discussion......Page 374
References......Page 375
Introduction......Page 376
Analysis of Approaches in Z......Page 377
Formal Templates for Relational Schemas......Page 382
Extending the Formal Template Language......Page 386
Conclusions......Page 387
Introduction......Page 390
Z Models and Alloy Instances......Page 392
A Semantics Preserving Translation for a Subset of Z......Page 395
More Z Constructs......Page 399
Schemas......Page 400
Discussion and Conclusion......Page 401
References......Page 402
B-ASM: Specification of ASM $\`{a} la$ B......Page 404
A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking......Page 405
References......Page 406
On the Modelling and Analysis of Amazon Web Services Access Policies......Page 407
Architecture as an Independent Variable for Aspect-Oriented Application Descriptions......Page 408
References......Page 409
Introducing Specification-Based Data Structure Repair Using Alloy......Page 411
Secrecy UML Method for Model Transformations......Page 413
Improving Traceability between KAOS Requirements Models and B Specifications......Page 414
References......Page 415
References......Page 416
References......Page 417
References......Page 418
References......Page 420
Reference......Page 421
References......Page 422
References......Page 423
References......Page 424
References......Page 425
References......Page 427
Author Index......Page 428

Details

  • Author: Marc Frappier, Uwe Glsser, Sarfraz Khurshid, Rgine Laleau, Steve Reeves
  • Publication Date: 2010
  • Publisher: Springer
  • ISBN-10: 3642118100
  • ISBN-13: 9783642118104
  • Pages: 429
  • Format: pdf
  • Size: 5.3M
Download Now Magnet