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

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

• Publisher: Springer
• Year: 2010
• Tongue: English
• Leaves: 517
• 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 Page
Preface
Organization
Table of Contents – Part II
EternalS: Mission and Roadmap
Introduction to the EternalS Track: Trustworthy Eternal Systems via Evolving Software, Data and Knowledge
HATS: Highly Adaptable and Trustworthy Software Using Formal Methods
Introduction
Mind the Gap
Main Results Achieved
SecureChange: Security Engineering for Lifelong Evolvable Systems
Introduction
The Project at a Glance
Key Results
3DLife: Bringing the Media Internet to Life
Introduction
Highlights of 3DLife Activities
Integration and Sustainability
Cooperative Research
Spreading Excellence
Conclusion
LivingKnowledge: Kernel Methods for Relational Learning and Semantic Modeling
The Data Representation Problem
Data Representation via Kernel Methods
Using Kernels for Semantic Inference in LivingKnowledge
Conclusion
References
Task Forces in the EternalS Coordination Action
Introduction
The EternalS Task Forces
Organization of EternalS Task Forces
Envisaged Outcomes of EternalS Task Forces
Conclusion
Modeling and Analyzing Diversity Description of EternalS Task Force 1
Introduction
Objectives and Vision
Organization and Work Plan
Conclusion
Modeling and Managing System Evolution Description of EternalS Task Force 2
Introduction
Vision
Objectives
Work Plan
Organization
Conclusion
Self-adaptation and Evolution by Learning Description of EternalS Task Force 3
Overview
Objectives and Vision
Organization and Work Plan
Conclusion
Overview of Roadmapping by EternalS
Introduction
Goals for the Roadmap
Approach
Initial Roadmap Mindmap
Relationship to Other Roadmapping Activity
Outlook
References
Formal Methods in Model-Driven Development for Service-Oriented and Cloud Computing
Adaptive Composition of Conversational Services through Graph Planning Encoding
Introduction
Preliminaries
Modeling
Conversation Modelling
Semantic Structures
Services
Composition Requirements
Encoding Composition as a Planning Problem
DSS Encoding
Workflow Encoding
Composition Requirements Encoding
Service Encoding
Overall Encoding
Plan Implementation
Tool Support
Related Work
Conclusion
References
Performance Prediction of Service-Oriented Systems with Layered Queueing Networks
Introduction
Modelling Services in UML4SOA
Mobile Payment Case Study
The Layered Queueing Model
LQN Models for UML4SOA
Performance Annotations with MARTE
Extracting the LQN Model
Indices of Performance
Numerical Example
Conclusion
References
Error Handling: From Theory to Practice
Introduction
SOCK
The Quest for Error Handling Primitives
Error Handling in SOCK
Full Specification
Expressiveness
Intuitiveness
Minimality
From SOCK to Jolie
Usability
Robustness
Compatibility
Property Preservation
Conclusion and Future Works
References
Modeling and Reasoning about Service Behaviors and Their Compositions
Introduction
Preliminaries
Remes Modeling Language
Guarded Command Language
Behavioral Modeling of Services in Remes
Hierarchical Language for Dynamic Service Composition: Syntax and Semantics
Example: An Autonomous Shuttle System
Modeling the Shuttle System in Remes
Applying the Hierarchical Language
Discussion and Related Work
Conclusions
References
Design and Verification of Systems with Exogenous Coordination Using Vereofy
Introduction
Constraint Automata
Specifying and Verifying Components and Connectors
Linear-Time Properties
Branching-Time Properties
Case Study: A Biomedical Sensor Network
The Model
Analysis of the Model
Conclusion
References
A Case Study in Model-Based Adaptation of Web Services
Introduction
Case Study: Online Medical Management System
Overview of the Adaptation Process
Interface Model Extraction
Adaptation Contract Specification
Generation of the Adaptor Protocol
Implementation
Concluding Remarks
References
Quantitative Verification in Practice
Quantitative Verification in Practice
Ten Years of Performance Evaluation for Concurrent Systems Using CADP
Introduction
The Interactive Markov Chain Model
The Interactive Probabilistic Chain Model
CADP Tools for Extended Markovian Models
State Space Generation Using CÆSAR.ADT and CÆSAR
Compositional Verification Using EXP.OPEN
Bisimulation Reduction Using BCG_MIN
Nondeterminism Elimination Using DETERMINATOR
Numerical Analysis Using BCG_STEADY and BCG_TRANSIENT
On-the-Fly Steady-State Simulation Using CUNCTATOR
Additional Tools for Interactive Probabilistic Chains
Applications
The Hubble Telescope Lifetime
Mutual Exclusion Protocols
The SCSI-2 Bus Arbitration Protocol
The MPI Send/Receive and Barrier Primitives
The xSTream Data-Flow Architecture
Conclusion and Future Work
References
Towards Dynamic Adaptation of Probabilistic Systems
Introduction
As-Is Situation: Deterministic Round Robin Service
To-Be Situation: Stationary Probabilistic Service
From Deterministic to Probabilistic Service
Adaptation Analysis with Prism
Conclusions
References
UPPAAL in Practice: Quantitative Verification of a RapidIO Network
Introduction
POOSL Model of a Realistic Motion Control System
Transformation from POOSL to UPPAAL
Data Part Transformation
Process Part Transformation
Heuristics
Scalability of the UPPAAL Model
Heuristics
Conclusions and Future Work
References
Schedulability Analysis Using Uppaal: Herschel-Planck Case Study
Introduction
The Herschel-Planck Mission
Model-Based Schedulability Methodology
Processor Scheduler
Tasks Templates
System Model Instantiation
Verification Queries
Results
Discussion
References
Model-Checking Temporal Properties of Real-Time HTL Programs
Introduction
The HTL2XTA Toolchain
Model Translation
Inference of Properties
Case Studies
Towards Correctness
Conclusion and Future Work
References
CONNECT: Status and Plans
Towards an Architecture for Runtime Interoperability
Introduction
Motivating Scenario: The Distributed Marketplace
Beyond State of the Art Interoperability Solutions
The Connect Architectural Framework
Discovery and Learning of Networked Systems
Synthesis of Connectors
Connect in Action
Conclusions and Future Work
References
On Handling Data in Automata Learning Considerations from the CONNECT Perspective
Introduction
Query Learning
The $L^*_M# Learning Algorithm
Practical Aspects in Active Learning
Connect Learning Challenges
Connect Model Requirements
Example
Experimental Results
Conclusion
References
A Theory of Mediators for Eternal Connectors
Introduction
Eternal Interoperability through Emergent Mediation
Definitions
Towards Emergent Mediators
The Popcorn Scenario
A Formalization of Protocols
Protocols as LTS
Abstract Protocol
Towards Automated Matching and Mediator Synthesis
Related Work
Conclusion
References
On-the-Fly Interoperability through Automated Mediator Synthesis and Monitoring
Introduction
Approach Description
Running Example
On-the-Fly Connector Synthesis and Monitoring
Automated Synthesis of Mediators
Automated Monitoring of Mediators
Conclusion
References
Dependability Analysis and Verification for Connected Systems
Introduction
Analysis and Verification Tools
PRISM
Möbius
The Distributed Market Scenario
Dependability Analysis and Verification
PRISM Models
Stochastic Verification
SAN Models
State-Based Stochastic Analysis
Conclusions
References
Towards a Connector Algebra
Introduction
Semantics for Connectors
Case Study
Towards a Connector Algebra: Primitives and Operators
Concluding Remarks
References
Certification of Software-Driven Medical Devices
Certification of Software-Driven Medical Devices
The Certification of Software-Driven Medical Devices Track
Reference
Arguing for Software Quality in an IEC 62304 Compliant Development Process
Introduction
Software Quality Assurance in Safety Standards
IEC 62304 - Process Requirements for Medical Device Software
IEC 61508-3 - Software Safety in E/E/EP Systems
Comparison
A Quality Model for Argumentations
A Staged Assessment Process
Structure and Well-Formedness Analysis
Conclusiveness of Argumentation
Assessment Procedure
Using the Quality Model for Assessment
Argument Review
Discussion
Conclusion
References
Trustable Formal Specification for Software Certification
Introduction
Overview of the Methodology
Case Study: A Cardiac Pacemaker
Benefits of Using Our Proposed Approach
Conclusion
References
Design Choices for High-Confidence Distributed Real-Time Software
Introduction
Mandatory Resource Reservation
Separation of Resource Consumptions
Enumerative Reconfiguration
Illustrative Example
Overview
Developing the Tree Schedule
Verifying the Tree Schedule
Simulating the System
Conclusion
References
Assurance Cases in Model-Driven Development of the Pacemaker Software
Introduction
Pacemaker Operation
Heart
Pacemaker
Model-Driven Development of Pacemaker Software
Overall Process
Formal Modeling
Formal Verification
Code Generation
Validation of the Generated Code
Assurance Cases
Discussion
Related Work
Conclusion
References
Modeling and Formalizing Industrial Software for Verification, Validation and Certification
Improving Portability of Linux Applications by Early Detection of Interoperability Issues
Introduction
Existing Approaches
Using a Testing Farm
OpenSUSE Build Service
Creating Standard-Compliant Applications
Static Analysis of Interfaces Involved in Interaction between Distributions and Applications
ELF Sections
Shared Libraries
Symbol Versions
Binary Symbols
Sufficient Requirement
Method Value
Linux Application Checker
Conclusion
References
Specification Based Conformance Testing for Email Protocols
Introduction
Related Works and Motivation
Mail Protocol Testing
UniTESK Technology Overview
The Proposed Method for Mail Protocols Conformance Testing
Method Application for Protocols SMTP, POP3 and IMAP4 Testing
Discussion
Results and Further Research
Further Research
Conclusion
References
Covering Arrays Generation Methods Survey
Introduction
Preliminaries
Survey of Algorithms for Covering Arrays Generation
Homogeneous Covering Arrays Generation Algorithms
Heterogeneous and Variable Depth Covering Arrays Generation Methods
Survey Results
Conclusion
References
Resource and Timing Analysis
A Scalable Approach for the Description of Dependencies in Hard Real-Time Systems
Introduction
Related Work
Real-Time Analysis
Model of Computation
Holistic Real-Time Analysis
Considering Dependencies
Mutual Exclusion
Offsets
Worst-Case Response Time Analysis with Limiting Event Streams
Example and Results
Conclusion
References
Verification of Printer Datapaths Using Timed Automata
Introduction
Case Study
Model Description
Verification
Conclusions
References
Resource Analysis of Automotive/Infotainment Systems Based on Domain-Specific Models – A Real-World Example
Introduction
Domain-Specific Modeling
The Hbsim DSL for Infotainment System Models
Example: Infotainment Head-Unit Startup
Model-Based Analysis and Simulation
Example Results
Conclusion and Next Steps
References
Source-Level Support for Timing Analysis
Introduction
Static Timing Analysis Techniques
Source-Level Analyses for Timing Analysis
The SATIrE Framework
High-Level Analyses Supporting Timing Analysis
Integration of Timing Analysis Tools
Integrated Compilation and WCET Calculation
Annotations for Measurement-Based Analysis
Annotations for Binary-Level Static Analysis
Integration with Other High-Level Tools
Source-Level Optimization and Timing Analysis
Transformation of Flow Information
Experimental Evaluation
Related Work
Conclusions
References
Practical Experiences of Applying Source-Level WCET Flow Analysis on Industrial Code
Introduction
Related Work
The ALL-TIMES Project
The Target System
Source Code Analysis Validation
SWEET, and Its Flow Analysis
Results and Experiences
Step 1: Identify Needed Source Files
Step 2: Converting Source Files
Step 3: Link the Converted Files
Step 4: Performing the Flow Analysis
Step 5: Map Results Back to Source Code
Conclusions
References
Worst-Case Analysis of Heap Allocations
Introduction
Related Work
WCET Analysis
Loop and Recursion Bounds
Data-Flow Analysis
Execution Time Calculation
Heap Allocation Analysis
Array Size Bounds
Object Layouts
Cost Functions
Evaluation
Results
JVM Comparison
Programming Style
Conclusion
References
Partial Flow Analysis with oRange
Introduction
Partial Analysis
Description
Automatization
Results
Conclusion
References
Towards an Evaluation Infrastructure for Automotive Multicore Real-Time Operating Systems
Problem
The Proposed Simulator
Related Work
Conclusion
References
Context-Sensitivity in IPET for Measurement-Based Timing Analysis
Introduction
Context-Dependent Execution Times
Evaluation
Conclusion and Outlook
References
On the Role of Non-functional Properties in Compiler Verification
Motivation
Classical Compiler Correctness
Compiler Correctness for PLCs
Related Work and Conclusions
References
Author Index