Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, ... I (Lecture Notes in Computer Science, 6415)

✍ Scribed by Tiziana Margaria (editor), Bernhard Steffen (editor)

• Publisher: Springer
• Year: 2010
• Tongue: English
• Leaves: 726
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

Title
Preface
Organization
Table of Contents – Part I
New Challenges in the Development of Critical Embedded Systems – An “aeromotive” Perspective
New Challenges in the Development of Critical Embedded Systems—An “aeromotive” Perspective
Certification of Embedded Software – Impact of ISODIS 26262 in the Automotive Domain
Enforcing Applicability of Real-Time Scheduling Theory Feasibility Tests with the Use of Design-Patterns
Introduction
The Design-Pattern Approach
Example of the Synchronous Data Flows Design-Pattern
Specification of the Synchronous Data Flows Design-Pattern
Feasibility Tests Assigned to the Synchronous Data Flows Design-Pattern
Example of an AADL Model Compliant with the Synchronous Data Flows Design-Pattern
A Decision Tool to Check the Compliance of an AADL Model with the Design-Patterns
Prototyping within Platypus
Design-Pattern Modeling Framework
Toward an Implementation within Cheddar
Related Works
Conclusion
References
Seamless Model-Driven Development Put into Practice
Introduction
Requirements for Seamless Model-Driven Development
Realization of Seamless Model-Driven Development
COLA – The Component Language
Model Analysis and System Synthesis
Tool Integration
Case Study
Related Work
Conclusion
References
Timely Time Estimates
Introduction
Framework
Code Instrumentation
Test Input Generation and Test Harness
Time Cost Repository and Hardware Benchmarking
Benchmark Selection
Time Estimation
Experiments
Related Work
Conclusion
References
Compiler-Support for Robust Multi-core Computing
Introduction
Robustness in Embedded Computing
Compiler Support for Robustness
Robustness in a Functional Setting
SAC - Data-Parallel Functional Programming
Support for Robustness with SAC
Discussion
References
Formal Languages and Methods for Designing and Verifying Complex Embedded Systems
Thematic Track: Formal Languages and Methods for Designing and Verifying Complex Embedded Systems
Analyzing the Security in the GSM Radio Network Using Attack Jungles
Introduction
Related Work
Outline
The Attack Jungle Formalism
Algorithm
Analyzing an Attack Jungle
Case Study: The GSM Network
The GSM System
Creating the GSM Attack Jungle
Analyzing the GSM Attack Jungle
Conclusion
References
Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method
Introduction
The OTS/CafeOBJ Method
Introduction to CafeOBJ
Observational Transition Systems
The SPINS Protocol Suite
The Sensor Network Encryption Protocol
The Node-to-Node Key Agreement Protocol
Formal Modeling and Verification of SNEP
Modeling
Verification
Formal Analysis of Node-to-Node Key Agreement Protocol
Lessons Learned
Related Work
Conclusions and Future Work
References
Model-Driven Design-Space Exploration for Embedded Systems: The Octopus Toolset
Introduction
Related Work
Motivating Example
The Octopus Architecture and Current Realization
DSEIR
Model Transformations
Transforming DSEIR Models to Coloured Petri Nets
Transforming DSEIR Models to Timed Automata
Case Studies
The Running Example
Modeling Printer Data Paths
Conclusions
References
Contract-Based Slicing
Introduction
Foundations: Verification Conditions and Specification-Based Slicing
Specification-Based Slicing
Open / Closed Contract-Based Slicing
Contract-Based Slicing: General Case
A Contract-Based Slicing Algorithm
An Illustrative Example
Conclusion
References
Worst-Case Traversal Time (WCTT)
Special Track on Worst Case Traversal Time (WCTT)
The PEGASE Project: Precise and Scalable Temporal Analysis for Aerospace Communication Systems with Network Calculus
Introduction
Industrial Context
Wide-Scale Communicating Systems
Shared Resources: Homogeneous vs. Heterogeneous Flows
Mono-Segment vs. Multi-hop (Homogeneous or Heterogeneous)
Use of Formal Methods in the Development Process
Related Works
Main Approaches to Timing Verification
Why Network Calculus Fits Embedded Systems
Network Calculus: An Overview of the State of the Art
Objectives and Novelty of the PEGASE Project
Case-Studies : AFDX, SpaceWire and NoC
AFDX
SpaceWire
Network on Chip
Some Theoretical Improvements
Model Hierarchy
Strict Priority Residual Services
Tight Results under Blind Policy
Complexity Problem
Tool Support
Requirements on the Tool
Design Considerations
Implementation
Tool Validation
Conclusion
References
NC-Maude: A Rewriting Tool to Play with Network Calculus
Introduction
Network Calculus
WhAT: Why Another Tool?
DISCO
COINC
CyNC
RTC
DEBORAH
PEGASE
NC-Maude Objectives
Why Rewriting?
NC-Maude
An Example of Interaction
NC-Maude Code Description
Extending NC-Maude
Licence
Conclusion
References
Example of Distance Between Theory and Implementation
DEBORAH: A Tool for Worst-Case Analysis of FIFO Tandems
Introduction
Network Calculus Background
System Model
The LUDB Methodology
DEBORAH
Nested Tandems
Non-nested Tandems
Lower Bounds
Using DEBORAH
Conclusions
References
A Self-adversarial Approach to Delay Analysis under Arbitrary Scheduling
Introduction
Motivation
Related Work
Contributions
Preliminaries on Network Calculus
Conventional Network Calculus and Non-FIFO Systems
Using Service Curves (SC) for Non-FIFO Systems
Using Strict Service Curves (S2C) for Non-FIFO Systems
The Self-adversarial Approach
The Self-adversarial Method
Self-adversarial vs. Additive Bounding Method
Numerical Experiments
Comparison of Self-adversarial and Additive Bounding
FIFO vs. Non-FIFO Delay Bounds
Conclusion and Discussion
References
Flow Control with (Min,+) Algebra
Introduction
An Algebraic Approach of Network Calculus
(Min,+) Algebra
Other Algebraic Preliminaries
Operations of Network Calculus
Network Calculus Modelling
Input and Output Flows, Arrival and Service Curves
Performance Characteristics: Delay and Backlog
Functions Associated to Delay and Backlog
Flow Control
Arrival Curve Computation
Window Flow Control
Application: Window Flow Control with a Given Delay
Configuration
Computation of the Arrival Curve \ˆ{α}*
Computation of the Window Size \ˆ {w}
Conclusion
References
An Interface Algebra for Estimating Worst-Case Traversal Times in Component Networks
Introduction
Timing Analysis of Component Networks
Processing Element
Playout Buffer
Earliest Deadline First Component
Worst-Case Traversal Times of Component Networks
Interface Algebra
Processing Element
Playout Buffer
Earliest Deadline First Component
Worst-Case Traversal Time Interface
Illustrative Example
Concluding Remarks
References
Appendix: Min-Max Algebra
Towards Resource-Optimal Routing Plans for Real-Time Traffic
Introduction
System Model
Scheduling and Latency
Path Computation Algorithms
Optimal Resource Allocation
Numerical Results
Conclusions and Future Work
References
Partially Synchronizing Periodic Flows with Offsets Improves Worst-Case End-to-End Delay Analysis of Switched Ethernet
Introduction
End-to-End Delay Analysis
Network and Traffic Model
Influence of Partial Synchronization
Worst-Case Delay Analysis with Partial Synchronization
Basic Network Calculus Approach for ETE Delay Analysis
Arrival Curves with Partial Synchronization of Flows
Evaluation of the Proposed Approach
Example of an Offset Assignment
Obtained Results
Conclusion and Future Work
References
Analyzing End-to-End Functional Delays on an IMA Platform
Introduction
Context
Objective: Evaluation of Functional Delays
Contribution
A Simplified Navigation and Guidance System
Formal modeling
The Model
Behavioral Description with Timed Automata
Analysis and Verification
Model-Checking Verification
A Mixed Verification Technique
Offset-Based Trajectory Approach
Conclusion and Perspectives
References
Tools in Scientific Workflow Composition
Tools in Scientific Workflow Composition
References
Workflows for Metabolic Flux Analysis: Data Integration and Human Interaction
Introduction
Metabolic Flux Analysis with Labeling Experiments
Scientific Workflow Applications in the 13C-MFA Domain
Aims of this Contribution
Ingredients for 13C-MFA
Model Editing and Visualization with Omix
High-Performance Simulation Toolbox: 13CFLUX2
Scientific Workflows for 13C-MFA
Metabolic Reaction Network Modeling Workflow
Graphical Network Modeling with Omix
Network Model Configuration
Simulation and Evaluation
Visualization
Implementation Details
Omix Plug-In Interface
Web Service Implementation of the Parameter Fitting Program
Conclusions
References
Intelligent Document Routing as a First Steptowards Workflow Automation: A Case Study Implemented in SQL
Introduction
Business and Data Understanding
Preprocessing and Exploratory Data Analysis
Modeling and Results
Implementation
Conclusions and Future Work
References
Combining Subgroup Discovery and Permutation Testing to Reduce Reduncancy
Introduction
Related Work
Ontologies
Annotations and Mappings
Related Algorithms
The Fantom Service
Ontologies
Mapping
Scoring
Output
Rule Generation
Rule Pruning
Exact Testing for Pruning and Optimization
Exact Testing: Single-Class Pruning Optimization
Exact Testing: Multi-class Threshold Optimization
Experimental Results
Exact Testing: Single-Class Pruning
Exact Testing: Multi-class Threshold Optimization
Conclusions and Future Work
References
Semantically-Guided Workflow Construction in Taverna: The SADI and BioMoby Plug-Ins
Introduction
BioMoby Semantic Web Services
SADI Semantic Web Services
The Taverna BioMoby and SADI Plugins
The BioMoby Plugin to Taverna
The SADI Plugin to Taverna
Semantic Service Discovery in Workflow Construction
Other BioMoby/SADI Web Service Composition Systems
References
Workflow Construction for Service-Oriented Knowledge Discovery
Introduction
Related Work
Orange4WS Platform
Design and Implementation
Production of New Web Services
Knowledge Discovery Ontology
Knowledge
Algorithms
Annotating Algorithms
Automated Workflow Construction
Exploiting Algorithm Hierarchy
A Framework for Workflow Execution in Orange4WS
A Text Mining Use Case
Conclusions
References
Workflow Composition and Enactment Using jORCA
Introduction
System and Methods
Results
Discussion
Conclusions
References
A Linked Data Approach to Sharing Workflows and Workflow Results
Introduction
Motivating Scenario
Bottlenecks for Evaluating a Bioinformatics Experiment
Semantic Web, RDF and Linked Data
Resources for Digital Materials and Methods
RDF: The Model for Linked Data and Comprehensive, Yet Light-Weight Coverage of Experiment-Related Data
myExperiment and BioCatalogue: Repositories for Digital Protocols and Their Components
Workflow and Provenance
Concept Web: Repository for Uniquely Identified Concepts, Their Relations and their Evidence
Proof of Principle
Linking Experimental Results and Evidence (Taverna Provenance),Personal Interpretation (AIDA Plugin), Digital Protocol (myExperiment) and Its Components (BioCatalogue), in Terms of Biological Concepts (ConceptWiki)
Discussion and Conclusion
Research Objects for Publication
References
Emerging Services and Technologies for a Converging Telecommunications / Web World in Smart Environments of the Internet of Things
Towards More Adaptive Voice Applications
Introduction
Background and Related Work
The (Mobile) Internet Today: When Best Effort Is Not Enough
Case Study: Adaptive Voice Communication
Discussion and Conclusion
References
Telco Service Delivery Platforms in the Last Decade - A R&D Perspective
Introduction
The New Service Delivery Platforms
…and the Network Operators?
Application Layer Multicast of Video on Demand Streams
A Location Service with Tunable Privacy
Quality of Service and Pricing
Concluding Remarks
References
Ontology-Driven Pervasive Service Composition for Everyday Life
Introduction
Fundamental Issues and Terminologies
Fundamental Issues
Terms in Business Integration
Terms Related to Ontology-Driven Pervasive Service Composition
Requirement Analysis
Requirements for Pervasive Service Composition
Ontology Model for Pervasive Service Composition
Survey of Web service Composition Approaches
Syntactic Web Service Composition
Semantic Web Service Composition
Conclusions and Future Work
References
Navigating the Web of Things: Visualizing and Interacting with Web-Enabled Objects
Introduction
An approach to the Web of Things
Related Work
Virtual Objects
Composing Objects of an Environment and Using Them in Applications
Towards New User Experience
Distinguishing Web-Enabled Objects from Non-connected Objects
Understanding Objects’ Behaviors
Grouping Objects
Illustration of the Web of Things Experience
Browsing Virtual Objects In-Situation
Browsing Virtual Objects Off-Situation
Conclusion
References
Shaping Future Service Environments with the Cloud and Internet of Things: Networking Challenges and Service Evolution
Introduction
Cloud Computing in the Telecom Perspectives
Ubiquitous Networking and Vision for the Internet of Things
Ubiquitous Networking for the Internet of Things
Interdisciplinary Fusion Revolution Crosses over Industries
The Cloud-Based Internet of Things
Future Networking Challenges and Service Evolution to Support the Internet of Things
Characteristics of Ubiquitous Networking for IoT
Enhanced Capabilities for Ubiquitous Networking in the Internet of Things Smart Environment
Service Evolution Using Smart Environment of the Cloud and the IoT
Conclusion
References
Relay Placement Problem in Smart Grid Deployment
Introduction to the Power Grid
Smart Grid
Advanced Metering Infrastructure (AMI)
How AMI Works
National Science Council Program in Taiwan
Factors That Affect Deployment Cost
Relay Placement Problem (RPP)
Problem Definition
The Worst Situation of Deployment
The Evaluation Criterion – Approximation Ratio
Approximation Algorithms and Variations of RPP
Decision Supporting System in NSC Program
Conclusions and Future Works
References
Web Science
Towards a Research Agenda for Enterprise Crowdsourcing
Introduction
Applications of Crowdsourcing in the Enterprise
Models of Crowdsourcing
Crowd Types
Incentives
Quality Assurance
Governance and Legal
Social Factors
Business Models and Viability
Summary
References
Analyzing Collaboration in Software Development Processes through Social Networks
Introduction
Software Development Models
Collaboration and Discipline
Social Networks
Requirements for Social Networks Tools
EvolTrack-SocialNetwork
Scenario of Collaboration Information Use
Conclusion
References
A Web-Based Framework for Collaborative Innovation
Introduction
Understanding CI
CI, Dynamic Asset Mapping and the Web
Constituents of CI and Dynamic Asset Mapping
Properties of Dynamic Asset Mapping CI
Implementing CI Based on Dynamic Asset Mapping
CI Examples Based on Dynamic Asset Mapping
CI Based Geomatics (Mapping)
CI Based on Dynamic Asset-Mapping for Geographic Communities - Family Service Toronto
Dynamic Asset-Mapping for Communities of Practice the Mennonite Heritage Portrait
Related Work
Conclusion
References
A Distributed Dynamics for WebGraph Decontamination
Introduction
Related Works
Edge Reversal Decontamination
Alg-Stretcher
Alg-Decontamination
Experimental Results
Conclusions
References
Increasing Users’ Trust on Personal Assistance Software Using a Domain-Neutral High-Level User Model
Introduction
A Domain-Neutral User Metamodel
A Two-Level Software Architecture for Building Personal Assistance Software
Detailing our Software Architecture
Instantiating Our User Metamodel for Different Application Domains
Related Work
Conclusion
References
Understanding IT Organizations
Introduction
Principles
Relevant Design Concepts
Contextual Design
Accountability
Trust and Reputation of Information Sources
Provenance and Traceability
Case-Based Reasoning
Proposed Metamodel
The Knowledge Elicitation Process
Document Reading
Interviews
Stakeholder Meetings
Ethnography
Related Work
Concluding Remarks
References
On the 2-Categorical View of Proofs
Introduction
Some 2-Categorical Notions
2-Category and Proof Theory
Conjunction
Disjunction
Implication
On the Interpretation for
Conclusion
References
Model Transformation and Analysis for Industrial Scale Validation
WOMM: A Weak Operational Memory Model
Introduction
Program Model
Operational Semantics
Structure of States
Execution
Complete Execution and Observable State
Semantics of Issue
Semantics of Commit
Abstract Execution
Relaxed Behaviors Allowed by WOMM
Relationship with Other Memory Models
The DRF Guarantee
Related Work
Conclusion and Future Work
References
Proof of Lemma 2
A Memory Model for Static Analysis of C Programs
Introduction
Name Binding Model
Array Simulation Model
Region Based Ternary Model
Region Hierarchy
Region Properties
Region Views
Simulation of C Semantics
Abstract Values
l-Value and r-Value
Evaluation Rules
An Example
Implementation
Related Work
Conclusion
References
Analysing Message Sequence Graph Specifications
Introduction
Message Sequence Charts
Transition System for an MSG
Reducing TG
Regularity of Com-Connected MSG's
Synchronous MSG's
Detecting Implied Scenarios
Conclusion
References
Optimize Context-Sensitive Andersen-Style Points-ToAnalysis by Method Summarization and Cycle-Elimination
Introduction
Method Summarization
Atomic Statements
Method Summary
The Framework of the Inter-Procedure Analysis
The Representation of Calling-Contexts
The Nodes and Edges of the Main Points-to Graph
Expanding Calling-Contexts
Computing the Transitive Closure of the Main Points-To Graph
Our Solution of Efficiency
Cycle Elimination and Node Collapse in the Main Points-To Graph
Optimization in Method Summaries
Experimental Result and Evaluation
Related Work
Conclusion
References
A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL
Introduction
Overview of WS-Atomic Transaction Protocol
Formalization and Modelling of the Protocol
The UPPAAL Model
Global Declarations
Messages
Initiator-Coordinator Process
Participant Process
Model Properties and Verification Results
Model Properties
Performance Results
Comparison and Conclusion
References
SPARDL: A Requirement Modeling Language for Periodic Control System
Introduction
The Requirement Modeling Language
Module-Hierarchy Syntax
Mode-Hierarchy Syntax
Operational Semantics for SPARDL
Configuration
Transition Rules
A Case Study
Requirement Prototype Generation
Tool Implementation
Discussion
Conclusion
References
AutoPA: Automatic Prototyping from Requirements
Introduction
The Library System
Modeling of requirements
UML Models of Requirements
Use Case Model
Design of AutoPA
Implementation of OCL Expressions
Prototype of the Library System
Generating a prototype
Execution of Generated Prototype
Conclusion and Discussion
References
Systematic Model-Based Safety Assessment Via Probabilistic Model Checking
Introduction
Overview of Quantitative Safety Assessment
Overview of Prism towards Safety Analysis
Proposed Strategy
Input Data Model
Translation Rules
Modeling Considerations
Case Study
Related Work
Conclusion
References
Learning Techniques for Software Verification and Validation
Learning Techniques for Software Verification and Validation – Special Track at ISoLA 2010
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning
Introduction
Preliminaries
The Learning Model
Learning a Contextual Assumption
Exact Learning Algorithms for Boolean Functions
The CDNF Algorithm
A Learning Algorithm for Ordered Binary Decision Diagrams
Experiments
Conclusion
References
Inferring Compact Models of Communication Protocol Entities
Introduction
Mealy Machines
Inference of Symbolic Mealy Machines
Inference of Mealy Machines
Generating Symbolic Representation of Mealy Machines
Implementation
Experiments
Results
Evaluation
Conclusions and Future Work
References
Inference and Abstraction of the Biometric Passport
Introduction
Overview
Inference and Abstraction of Mealy Machines
Mealy Machines
Inference of Mealy Machines
Inference Using Abstraction
Biometric Passport
Experiments
Abstraction Mapping
Results
The Behavior of the SUT
Validation
Conclusions and Future Work
References
From ZULU to RERS Lessons Learned in the ZULU Challenge
Motivation
Active Learning
The ZULU Competition
A Configurable Inference Framework
Continuous Equivalence Queries
Results
Discussion of the ZULU Rating Approach
RERS - Regular Inference of Reactive Systems
Conclusion
References
Author Index