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

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. 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