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 I

Cover\r......Page 1
Preface......Page 6
Organization......Page 8
Table of Contents – Part I......Page 10
Table of Contents – Part II......Page 16
New Challenges in the Development of Critical Embedded Systems—An “aeromotive” Perspective......Page 21
Certification of Embedded Software – Impact of ISO DIS 26262 in the Automotive Domain......Page 23
Introduction......Page 24
The Design-Pattern Approach......Page 25
Specification of the [\\it Synchronous Data Flows} Design-Pattern......Page 27
Feasibility Tests Assigned to the {\\it Synchronous Data Flows} Design-Pattern......Page 28
Example of an AADL Model Compliant with the {\\it Synchronous  Data Flows} Design-Pattern......Page 29
A Decision Tool to Check the Compliance of an AADL Model with the Design-Patterns......Page 30
Prototyping within Platypus......Page 31
Design-Pattern Modeling Framework......Page 32
Related Works......Page 34
Conclusion......Page 35
References......Page 36
Introduction......Page 38
Requirements for Seamless Model-Driven Development......Page 39
Realization of Seamless Model-Driven Development......Page 40
COLA – The Component Language......Page 41
Model Analysis and System Synthesis......Page 44
Tool Integration......Page 47
Case Study......Page 49
Related Work......Page 50
References......Page 51
Introduction......Page 53
Framework......Page 55
Code Instrumentation......Page 56
Test Input Generation and Test Harness......Page 57
Benchmark Selection......Page 60
Time Estimation......Page 61
Experiments......Page 62
Related Work......Page 63
Conclusion......Page 64
References......Page 65
Introduction......Page 67
Robustness in Embedded Computing......Page 68
Compiler Support for Robustness......Page 69
Robustness in a Functional Setting......Page 71
SAC - Data-Parallel Functional Programming......Page 72
Support for Robustness with SAC......Page 74
References......Page 75
Thematic Track: Formal Languages and Methods for Designing and Verifying Complex Embedded Systems......Page 78
Introduction......Page 80
Related Work......Page 81
The Attack Jungle Formalism......Page 82
Algorithm......Page 84
Analyzing an Attack Jungle......Page 85
The GSM System......Page 88
Analyzing the GSM Attack Jungle......Page 90
Conclusion......Page 92
References......Page 93
Introduction......Page 95
Observational Transition Systems......Page 96
The SPINS Protocol Suite......Page 97
The Sensor Network Encryption Protocol......Page 98
Modeling......Page 99
Verification......Page 103
Formal Analysis of Node-to-Node Key Agreement Protocol......Page 104
Lessons Learned......Page 105
Related Work......Page 107
References......Page 108
Introduction......Page 110
Related Work......Page 112
Motivating Example......Page 113
The Octopus Architecture and Current Realization......Page 114
DSEIR......Page 115
Transforming DSEIR Models to Coloured Petri Nets......Page 118
Transforming DSEIR Models to Timed Automata......Page 119
The Running Example......Page 120
Modeling Printer Data Paths......Page 122
Conclusions......Page 123
References......Page 124
Introduction......Page 126
Foundations: Verification Conditions and Specification-Based Slicing......Page 127
Specification-Based Slicing......Page 130
Open / Closed Contract-Based Slicing......Page 132
Contract-Based Slicing: General Case......Page 134
A Contract-Based Slicing Algorithm......Page 135
An Illustrative Example......Page 136
Conclusion......Page 139
References......Page 140
Special Track on Worst Case Traversal Time (WCTT)......Page 141
Introduction......Page 142
Shared Resources: Homogeneous vs. Heterogeneous Flows......Page 143
Related Works......Page 144
Main Approaches to Timing Verification......Page 145
Network Calculus: An Overview of the State of the Art......Page 146
Objectives and Novelty of the PEGASE Project......Page 147
AFDX......Page 149
Network on Chip......Page 150
Strict Priority Residual Services......Page 151
Requirements on the Tool......Page 152
Tool Validation......Page 153
References......Page 154
Introduction......Page 157
Network Calculus......Page 158
DISCO......Page 160
RTC......Page 161
NC-Maude Objectives......Page 162
Why Rewriting?......Page 163
An Example of Interaction......Page 164
NC-Maude Code Description......Page 166
Extending NC-Maude......Page 167
Conclusion......Page 168
References......Page 169
Example of Distance Between Theory and Implementation......Page 170
Introduction......Page 172
Network Calculus Background......Page 173
System Model......Page 175
The LUDB Methodology......Page 177
Nested Tandems......Page 179
Non-nested Tandems......Page 181
Lower Bounds......Page 182
Using DEBORAH......Page 185
References......Page 187
Motivation......Page 189
Related Work......Page 191
Preliminaries on Network Calculus......Page 192
Using Service Curves (SC) for Non-FIFO Systems......Page 194
Using Strict Service Curves (S2C) for Non-FIFO Systems......Page 195
The Self-adversarial Method......Page 197
Self-adversarial vs. Additive Bounding Method......Page 198
FIFO vs. Non-FIFO Delay Bounds......Page 200
Conclusion and Discussion......Page 201
References......Page 202
Introduction......Page 204
(Min,+) Algebra......Page 205
Operations of Network Calculus......Page 206
Input and Output Flows, Arrival and Service Curves......Page 208
Performance Characteristics: Delay and Backlog......Page 209
Functions Associated to Delay and Backlog......Page 211
Arrival Curve Computation......Page 212
Window Flow Control......Page 213
Computation of the Arrival Curve $\\^{α}^*$......Page 215
Conclusion......Page 216
References......Page 217
Introduction......Page 218
Processing Element......Page 220
Playout Buffer......Page 221
Earliest Deadline First Component......Page 222
Interface Algebra......Page 223
Processing Element......Page 226
Earliest Deadline First Component......Page 227
Worst-Case Traversal Time Interface......Page 228
Illustrative Example......Page 229
Concluding Remarks......Page 231
References......Page 232
Appendix: Min-Max Algebra......Page 233
Introduction......Page 234
System Model......Page 236
Scheduling and Latency......Page 237
Path Computation Algorithms......Page 238
Optimal Resource Allocation......Page 239
Numerical Results......Page 242
Conclusions and Future Work......Page 245
References......Page 246
Introduction......Page 248
Influence of Partial Synchronization......Page 249
Basic Network Calculus Approach for ETE Delay Analysis......Page 252
Arrival Curves with Partial Synchronization of Flows......Page 254
Example of an Offset Assignment......Page 257
Obtained Results......Page 258
References......Page 261
Context......Page 263
Contribution......Page 264
A Simplified Navigation and Guidance System......Page 266
The Model......Page 267
Behavioral Description with Timed Automata......Page 268
Model-Checking Verification......Page 270
A Mixed Verification Technique......Page 271
Offset-Based Trajectory Approach......Page 273
References......Page 276
Tools in Scientific Workflow Composition......Page 278
References......Page 280
Introduction......Page 281
Metabolic Flux Analysis with Labeling Experiments......Page 282
Scientific Workflow Applications in the 13C-MFA Domain......Page 283
Model Editing and Visualization with Omix......Page 284
Metabolic Reaction Network Modeling Workflow......Page 285
Graphical Network Modeling with Omix......Page 287
Network Model Configuration......Page 288
Visualization......Page 289
Implementation Details......Page 290
Web Service Implementation of the Parameter Fitting Program......Page 291
Conclusions......Page 293
References......Page 294
Introduction......Page 296
Business and Data Understanding......Page 298
Preprocessing and Exploratory Data Analysis......Page 300
Modeling and Results......Page 301
Conclusions and Future Work......Page 302
References......Page 304
Introduction......Page 305
Ontologies......Page 306
Related Algorithms......Page 307
Scoring......Page 308
Rule Pruning......Page 309
Exact Testing: Single-Class Pruning Optimization......Page 310
Exact Testing: Multi-class Threshold Optimization......Page 311
Exact Testing: Single-Class Pruning......Page 313
Exact Testing: Multi-class Threshold Optimization......Page 315
Conclusions and Future Work......Page 317
References......Page 318
Introduction......Page 321
BioMoby Semantic Web Services......Page 322
SADI Semantic Web Services......Page 323
The Taverna BioMoby and SADI Plugins......Page 324
The BioMoby Plugin to Taverna......Page 325
The SADI Plugin to Taverna......Page 327
Semantic Service Discovery in Workflow Construction......Page 329
Other BioMoby/SADI Web Service Composition Systems......Page 330
References......Page 331
Introduction......Page 333
Related Work......Page 334
Design and Implementation......Page 335
Knowledge Discovery Ontology......Page 337
Knowledge......Page 338
Annotating Algorithms......Page 339
Exploiting Algorithm Hierarchy......Page 340
A Framework for Workflow Execution in Orange4WS......Page 341
A Text Mining Use Case......Page 342
References......Page 345
Introduction......Page 348
System and Methods......Page 349
Results......Page 352
Discussion......Page 353
Conclusions......Page 357
References......Page 358
A Linked Data Approach to Sharing Workflows and Workflow Results......Page 360
Motivating Scenario......Page 361
Bottlenecks for Evaluating a Bioinformatics Experiment......Page 362
Semantic Web, RDF and Linked Data......Page 364
Resources for Digital Materials and Methods......Page 365
myExperiment and BioCatalogue: Repositories for Digital Protocols and Their Components......Page 366
Workflow and Provenance......Page 367
Concept Web: Repository for Uniquely Identified Concepts, Their Relations and their Evidence......Page 368
Linking Experimental Results and Evidence (Taverna Provenance),Personal Interpretation (AIDA Plugin), Digital Protocol (myExperiment) and Its Components (BioCatalogue), in Terms of Biological Concepts (ConceptWiki)......Page 369
Discussion and Conclusion......Page 371
Research Objects for Publication......Page 372
References......Page 373
Introduction......Page 375
Background and Related Work......Page 376
The (Mobile) Internet Today: When Best Effort Is Not Enough......Page 377
Case Study: Adaptive Voice Communication......Page 379
Discussion and Conclusion......Page 383
References......Page 384
Introduction......Page 387
The New Service Delivery Platforms......Page 390
Application Layer Multicast of Video on Demand Streams......Page 391
A Location Service with Tunable Privacy......Page 392
Concluding Remarks......Page 393
References......Page 394
Introduction......Page 395
Fundamental Issues......Page 396
Terms in Business Integration......Page 397
Terms Related to Ontology-Driven Pervasive Service Composition......Page 399
Requirements for Pervasive Service Composition......Page 401
Ontology Model for Pervasive Service Composition......Page 403
Survey of Web service Composition Approaches......Page 404
Semantic Web Service Composition......Page 405
Conclusions and Future Work......Page 406
References......Page 407
Introduction......Page 410
Related Work......Page 411
Composing Objects of an Environment and Using Them in Applications......Page 412
Distinguishing Web-Enabled Objects from Non-connected Objects......Page 413
Grouping Objects......Page 414
Browsing Virtual Objects In-Situation......Page 415
Browsing Virtual Objects Off-Situation......Page 416
References......Page 417
Introduction......Page 419
Cloud Computing in the Telecom Perspectives......Page 421
Ubiquitous Networking and Vision for the Internet of Things......Page 422
Ubiquitous Networking for the Internet of Things......Page 423
Interdisciplinary Fusion Revolution Crosses over Industries......Page 424
The Cloud-Based Internet of Things......Page 425
Characteristics of Ubiquitous Networking for IoT......Page 426
Enhanced Capabilities for Ubiquitous Networking in the Internet of Things Smart Environment......Page 427
Service Evolution Using Smart Environment of the Cloud and the IoT......Page 428
References......Page 429
Introduction to the Power Grid......Page 431
Smart Grid......Page 432
How AMI Works......Page 435
National Science Council Program in Taiwan......Page 436
Factors That Affect Deployment Cost......Page 437
Problem Definition......Page 438
The Worst Situation of Deployment......Page 439
Approximation Algorithms and Variations of RPP......Page 441
Decision Supporting System in NSC Program......Page 442
Conclusions and Future Works......Page 443
References......Page 444
Introduction......Page 445
Applications of Crowdsourcing in the Enterprise......Page 446
Models of Crowdsourcing......Page 447
Crowd Types......Page 448
Incentives......Page 449
Quality Assurance......Page 450
Governance and Legal......Page 451
Business Models and Viability......Page 452
References......Page 453
Introduction......Page 455
Software Development Models......Page 456
Collaboration and Discipline......Page 457
Social Networks......Page 458
Requirements for Social Networks Tools......Page 459
EvolTrack-SocialNetwork......Page 460
Scenario of Collaboration Information Use......Page 462
Conclusion......Page 463
References......Page 464
Introduction......Page 467
Understanding CI......Page 469
Constituents of CI and Dynamic Asset Mapping......Page 470
Properties of Dynamic Asset Mapping CI......Page 472
Implementing CI Based on Dynamic Asset Mapping......Page 473
CI Based Geomatics (Mapping)......Page 475
CI Based on Dynamic Asset-Mapping for Geographic Communities - Family Service Toronto......Page 476
Dynamic Asset-Mapping for Communities of Practice the Mennonite Heritage Portrait......Page 478
Related Work......Page 479
References......Page 480
Introduction......Page 482
Related Works......Page 484
Alg-Stretcher......Page 485
Alg-Decontamination......Page 487
Experimental Results......Page 489
Conclusions......Page 490
References......Page 491
Introduction......Page 493
A Domain-Neutral User Metamodel......Page 495
A Two-Level Software Architecture for Building Personal Assistance Software......Page 500
Detailing our Software Architecture......Page 501
Instantiating Our User Metamodel for Different Application Domains......Page 503
Conclusion......Page 505
References......Page 506
Introduction......Page 508
Principles......Page 509
Contextual Design......Page 510
Trust and Reputation of Information Sources......Page 512
Provenance and Traceability......Page 513
Case-Based Reasoning......Page 514
Proposed Metamodel......Page 515
Document Reading......Page 517
Ethnography......Page 518
Related Work......Page 519
References......Page 520
Introduction......Page 522
Some 2-Categorical Notions......Page 524
2-Category and Proof Theory......Page 525
Conjunction......Page 526
Disjunction......Page 530
Implication......Page 533
On the Interpretation for......Page 536
Conclusion......Page 537
References......Page 538
Introduction......Page 539
Program Model......Page 541
Structure of States......Page 542
Execution......Page 543
Semantics of Issue......Page 544
Semantics of Commit......Page 545
Abstract Execution......Page 548
Relaxed Behaviors Allowed by WOMM......Page 549
Relationship with Other Memory Models......Page 550
The DRF Guarantee......Page 551
Related Work......Page 552
References......Page 553
Proof of Lemma 2......Page 554
Introduction......Page 555
Array Simulation Model......Page 556
Region Based Ternary Model......Page 557
Region Properties......Page 558
Region Views......Page 559
l-Value and r-Value......Page 560
Evaluation Rules......Page 561
An Example......Page 564
Implementation......Page 565
Related Work......Page 566
References......Page 567
Introduction......Page 569
Message Sequence Charts......Page 572
Transition System for an MSG......Page 574
Reducing TG......Page 577
Regularity of Com-Connected MSG\'s......Page 579
Synchronous MSG\'s......Page 580
References......Page 582
Introduction......Page 584
Atomic Statements......Page 586
Method Summary......Page 587
The Representation of Calling-Contexts......Page 589
Expanding Calling-Contexts......Page 590
Computing the Transitive Closure of the Main Points-To Graph......Page 591
Cycle Elimination and Node Collapse in the Main Points-To Graph......Page 592
Optimization in Method Summaries......Page 594
Experimental Result and Evaluation......Page 596
Conclusion......Page 597
References......Page 598
Introduction......Page 599
Overview of WS-Atomic Transaction Protocol......Page 600
Formalization and Modelling of the Protocol......Page 601
Global Declarations......Page 604
Initiator-Coordinator Process......Page 606
Participant Process......Page 607
Model Properties......Page 608
Performance Results......Page 610
Comparison and Conclusion......Page 611
References......Page 613
Introduction......Page 614
Module-Hierarchy Syntax......Page 616
Mode-Hierarchy Syntax......Page 617
Configuration......Page 618
Transition Rules......Page 619
A Case Study......Page 622
Requirement Prototype Generation......Page 623
Tool Implementation......Page 625
Discussion......Page 626
Conclusion......Page 627
References......Page 628
Introduction......Page 629
Modeling of requirements......Page 630
Use Case Model......Page 631
Design of AutoPA......Page 634
Implementation of OCL Expressions......Page 636
Prototype of the Library System......Page 638
Generating a prototype......Page 639
Execution of Generated Prototype......Page 640
Conclusion and Discussion......Page 642
References......Page 643
Introduction......Page 645
Overview of Quantitative Safety Assessment......Page 646
Overview of Prism towards Safety Analysis......Page 648
Proposed Strategy......Page 649
Input Data Model......Page 650
Translation Rules......Page 651
Modeling Considerations......Page 654
Case Study......Page 655
Related Work......Page 657
Conclusion......Page 658
References......Page 659
Learning Techniques for Software Verification and Validation – Special Track at ISoLA 2010......Page 660
Introduction......Page 663
Preliminaries......Page 665
The Learning Model......Page 666
Learning a Contextual Assumption......Page 667
The CDNF Algorithm......Page 670
A Learning Algorithm for Ordered Binary Decision Diagrams......Page 671
Experiments......Page 672
References......Page 676
Introduction......Page 678
Mealy Machines......Page 680
Inference of Symbolic Mealy Machines......Page 682
Generating Symbolic Representation of Mealy Machines......Page 683
Experiments......Page 686
Results......Page 687
Evaluation......Page 688
Conclusions and Future Work......Page 690
References......Page 691
Introduction......Page 693
Overview......Page 694
Inference and Abstraction of Mealy Machines......Page 695
Mealy Machines......Page 696
Inference Using Abstraction......Page 697
Biometric Passport......Page 698
Experiments......Page 699
Results......Page 700
The Behavior of the SUT......Page 702
Validation......Page 703
Conclusions and Future Work......Page 704
References......Page 705
Motivation......Page 707
Active Learning......Page 708
The ZULU Competition......Page 709
A Configurable Inference Framework......Page 711
Continuous Equivalence Queries......Page 713
Discussion of the ZULU Rating Approach......Page 716
RERS - Regular Inference of Reactive Systems......Page 719
References......Page 722
Author Index\r......Page 725