Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II

✍ Scribed by Tiziana Margaria, Bernhard Steffen

• Publisher: Springer
• Year: 2010
• Tongue: English
• Leaves: 520
• Edition: 1st Edition.
• Category: Library

✦ Synopsis

The two volume set LNCS 6415 and LNCS 6416 constitutes the refereed proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2010, held in Heraklion, Crete, Greece, in October 2010. The 100 revised full papers presented were carefully revised and selected from numerous submissions and discuss issues related to the adoption and use of rigorous tools and methods for the specification, analysis, verification, certification, construction, test, and maintenance of systems. The 46 papers of the first volume are organized in topical sections on new challenges in the development of critical embedded systems, formal languages and methods for designing and verifying complex embedded systems, worst-case traversal time (WCTT), tools in scientific workflow composition, emerging services and technologies for a converging telecommunications / Web world in smart environments of the internet of things, Web science, model transformation and analysis for industrial scale validation, and learning techniques for software verification and validation. The second volume presents 54 papers addressing the following topics: EternalS: mission and roadmap, formal methods in model-driven development for service-oriented and cloud computing, quantitative verification in practice, CONNECT: status and plans, certification of software-driven medical devices, modeling and formalizing industrial software for verification, validation and certification, and resource and timing analysis.

✦ Table of Contents

Cover
......Page 1
Preface......Page 6
Organization......Page 8
Table of Contents – Part II......Page 10
Table of Contents – Part I......Page 16
front-matter......Page 3
Introduction to the EternalS Track: Trustworthy Eternal Systems via Evolving Software, Data and Knowledge......Page 21
Mind the Gap......Page 23
Main Results Achieved......Page 26
Introduction......Page 29
The Project at a Glance......Page 30
Key Results......Page 31
Integration and Sustainability......Page 33
Conclusion......Page 34
The Data Representation Problem......Page 35
Data Representation via Kernel Methods......Page 36
Using Kernels for Semantic Inference in LivingKnowledge......Page 37
Conclusion......Page 38
References......Page 39
The EternalS Task Forces......Page 40
Organization of EternalS Task Forces......Page 41
Conclusion......Page 42
Objectives and Vision......Page 43
Organization and Work Plan......Page 44
Conclusion......Page 45
Introduction......Page 46
Work Plan......Page 47
Conclusion......Page 49
Objectives and Vision......Page 50
Conclusion......Page 51
Approach......Page 52
Relationship to Other Roadmapping Activity......Page 53
References......Page 54
Introduction......Page 55
Preliminaries......Page 56
Modeling......Page 57
Semantic Structures......Page 58
Services......Page 59
DSS Encoding......Page 61
Composition Requirements Encoding......Page 62
Service Encoding......Page 63
Plan Implementation......Page 64
Tool Support......Page 65
Related Work......Page 66
Conclusion......Page 67
References......Page 68
Introduction......Page 71
Modelling Services in UML4SOA......Page 72
Mobile Payment Case Study......Page 74
The Layered Queueing Model......Page 76
Performance Annotations with MARTE......Page 78
Extracting the LQN Model......Page 80
Numerical Example......Page 82
References......Page 84
Introduction......Page 86
SOCK......Page 88
The Quest for Error Handling Primitives......Page 89
Error Handling in SOCK......Page 90
Full Specification......Page 92
Expressiveness......Page 93
Minimality......Page 94
From SOCK to Jolie......Page 95
Usability......Page 96
Compatibility......Page 97
Property Preservation......Page 98
References......Page 99
Introduction......Page 102
REMES Modeling Language......Page 103
Guarded Command Language......Page 104
Behavioral Modeling of Services in REMES......Page 105
Hierarchical Language for Dynamic Service Composition: Syntax and Semantics......Page 108
Example: An Autonomous Shuttle System......Page 111
Modeling the Shuttle System in REMES......Page 112
Applying the Hierarchical Language......Page 113
Discussion and Related Work......Page 114
References......Page 115
Introduction......Page 117
Constraint Automata......Page 119
Linear-Time Properties......Page 121
Branching-Time Properties......Page 122
Case Study: A Biomedical Sensor Network......Page 124
The Model......Page 125
Analysis of the Model......Page 127
References......Page 130
Introduction......Page 132
Interface Model Extraction......Page 134
Adaptation Contract Specification......Page 136
Generation of the Adaptor Protocol......Page 140
Implementation......Page 141
Concluding Remarks......Page 145
References......Page 146
Quantitative Verification in Practice......Page 147
Introduction......Page 148
The Interactive Markov Chain Model......Page 149
The Interactive Probabilistic Chain Model......Page 151
CADP Tools for Extended Markovian Models......Page 152
State Space Generation Using CÆSAR.ADT and CÆSAR......Page 153
Nondeterminism Elimination Using DETERMINATOR......Page 154
Numerical Analysis Using BCG_STEADY and BCG_TRANSIENT......Page 155
Additional Tools for Interactive Probabilistic Chains......Page 156
The Hubble Telescope Lifetime......Page 157
The SCSI-2 Bus Arbitration Protocol......Page 158
The xSTream Data-Flow Architecture......Page 159
Conclusion and Future Work......Page 160
References......Page 161
Introduction......Page 163
As-Is Situation: Deterministic Round Robin Service......Page 165
To-Be Situation: Stationary Probabilistic Service......Page 168
From Deterministic to Probabilistic Service......Page 170
Adaptation Analysis with Prism......Page 174
Conclusions......Page 177
References......Page 178
Introduction......Page 180
POOSL Model of a Realistic Motion Control System......Page 182
Process Part Transformation......Page 186
Scalability of the UPPAAL Model......Page 190
Heuristics......Page 191
Conclusions and Future Work......Page 193
References......Page 194
Introduction......Page 195
The Herschel-Planck Mission......Page 196
Model-Based Schedulability Methodology......Page 199
Processor Scheduler......Page 200
Tasks Templates......Page 201
System Model Instantiation......Page 204
Results......Page 206
Discussion......Page 208
References......Page 209
Introduction......Page 211
The HTL2XTA Toolchain......Page 214
Model Translation......Page 215
Inference of Properties......Page 219
Case Studies......Page 221
Towards Correctness......Page 223
Conclusion and Future Work......Page 224
References......Page 225
Introduction......Page 226
Motivating Scenario: The Distributed Marketplace......Page 228
Beyond State of the Art Interoperability Solutions......Page 230
Discovery and Learning of Networked Systems......Page 232
Synthesis of Connectors......Page 234
Connect in Action......Page 235
Conclusions and Future Work......Page 238
References......Page 239
Introduction......Page 241
The $L^*_M$ Learning Algorithm......Page 242
Practical Aspects in Active Learning......Page 245
Connect Model Requirements......Page 247
Example......Page 250
Experimental Results......Page 251
Conclusion......Page 253
References......Page 254
Introduction......Page 256
Towards Emergent Mediators......Page 258
The Popcorn Scenario......Page 259
Protocols as LTS......Page 261
Abstract Protocol......Page 263
Towards Automated Matching and Mediator Synthesis......Page 265
Related Work......Page 267
Conclusion......Page 268
References......Page 269
Introduction......Page 271
Running Example......Page 273
On-the-Fly Connector Synthesis and Monitoring......Page 274
Automated Synthesis of Mediators......Page 276
Automated Monitoring of Mediators......Page 278
Conclusion......Page 280
References......Page 281
Introduction......Page 283
Analysis and Verification Tools......Page 284
PRISM......Page 285
Möbius......Page 286
The Distributed Market Scenario......Page 287
Stochastic Verification......Page 289
SAN Models......Page 292
State-Based Stochastic Analysis......Page 293
References......Page 296
Introduction......Page 298
Semantics for Connectors......Page 300
Case Study......Page 303
Towards a Connector Algebra: Primitives and Operators......Page 304
Concluding Remarks......Page 310
References......Page 311
The Certification of Software-Driven Medical Devices Track......Page 313
Reference......Page 315
Introduction......Page 316
IEC 62304 - Process Requirements for Medical Device Software......Page 317
IEC 61508-3 - Software Safety in E/E/EP Systems......Page 318
Comparison......Page 319
Structure and Well-Formedness Analysis......Page 320
Conclusiveness of Argumentation......Page 322
Assessment Procedure......Page 326
Using the Quality Model for Assessment......Page 327
Argument Review......Page 328
Conclusion......Page 329
References......Page 330
Introduction......Page 332
Overview of the Methodology......Page 335
Case Study: A Cardiac Pacemaker......Page 339
Benefits of Using Our Proposed Approach......Page 343
Conclusion......Page 344
References......Page 345
Introduction......Page 347
Mandatory Resource Reservation......Page 348
Separation of Resource Consumptions......Page 351
Enumerative Reconfiguration......Page 353
Illustrative Example......Page 354
Developing the Tree Schedule......Page 355
Verifying the Tree Schedule......Page 357
Simulating the System......Page 358
Conclusion......Page 359
References......Page 360
Introduction......Page 363
Heart......Page 364
Pacemaker......Page 365
Formal Modeling......Page 366
Code Generation......Page 368
Assurance Cases......Page 369
Discussion......Page 373
Related Work......Page 374
References......Page 375
Introduction......Page 377
Existing Approaches......Page 378
OpenSUSE Build Service......Page 379
Creating Standard-Compliant Applications......Page 380
Static Analysis of Interfaces Involved in Interaction between Distributions and Applications......Page 381
Shared Libraries......Page 383
Symbol Versions......Page 384
Binary Symbols......Page 385
Method Value......Page 386
Linux Application Checker......Page 387
Conclusion......Page 388
References......Page 389
Introduction......Page 391
Related Works and Motivation......Page 392
Mail Protocol Testing......Page 394
UniTESK Technology Overview......Page 396
The Proposed Method for Mail Protocols Conformance Testing......Page 397
Method Application for Protocols SMTP, POP3 and IMAP4 Testing......Page 398
Discussion......Page 399
Conclusion......Page 400
References......Page 401
Introduction......Page 402
Preliminaries......Page 404
Survey of Algorithms for Covering Arrays Generation......Page 405
Homogeneous Covering Arrays Generation Algorithms......Page 406
Heterogeneous and Variable Depth Covering Arrays Generation Methods......Page 408
Survey Results......Page 413
References......Page 414
Introduction......Page 417
Related Work......Page 418
Model of Computation......Page 419
Considering Dependencies......Page 421
Mutual Exclusion......Page 423
Offsets......Page 425
Worst-Case Response Time Analysis with Limiting Event Streams......Page 426
Example and Results......Page 428
References......Page 430
Introduction......Page 432
Case Study......Page 434
Model Description......Page 437
Verification......Page 438
References......Page 442
Introduction......Page 444
The Hbsim DSL for Infotainment System Models......Page 445
Example: Infotainment Head-Unit Startup......Page 448
Model-Based Analysis and Simulation......Page 449
Example Results......Page 451
Conclusion and Next Steps......Page 452
References......Page 453
Introduction......Page 454
Static Timing Analysis Techniques......Page 455
The SATIrE Framework......Page 456
High-Level Analyses Supporting Timing Analysis......Page 457
Annotations for Measurement-Based Analysis......Page 460
Annotations for Binary-Level Static Analysis......Page 461
Source-Level Optimization and Timing Analysis......Page 462
Transformation of Flow Information......Page 463
Experimental Evaluation......Page 464
References......Page 466
Introduction......Page 469
Related Work......Page 471
The ALL-TIMES Project......Page 472
Source Code Analysis Validation......Page 474
SWEET, and Its Flow Analysis......Page 475
Results and Experiences......Page 476
Step 2: Converting Source Files......Page 477
Step 4: Performing the Flow Analysis......Page 478
Step 5: Map Results Back to Source Code......Page 480
References......Page 481
Introduction......Page 484
Related Work......Page 485
WCET Analysis......Page 486
Data-Flow Analysis......Page 487
Heap Allocation Analysis......Page 488
Object Layouts......Page 489
Cost Functions......Page 490
Evaluation......Page 493
Results......Page 494
JVM Comparison......Page 495
Programming Style......Page 496
References......Page 497
Introduction......Page 499
Automatization......Page 500
Results......Page 501
References......Page 502
Problem......Page 503
The Proposed Simulator......Page 504
References......Page 506
Introduction......Page 507
Context-Dependent Execution Times......Page 508
References......Page 510
Motivation......Page 511
Classical Compiler Correctness......Page 512
Compiler Correctness for PLCs......Page 513
References......Page 514
Author Index
......Page 517