Leveraging applications of formal methods, verification and validation : technologies for mastering change ; 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings. Part I

The two-volume set LNCS 7609 and 7610 constitutes the thoroughly refereed proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, held in Heraklion, Crete, Greece, in October 2012. The two volumes contain papers presented in the topical sections on adaptable and evolving software for eternal systems, approaches for mastering change, runtime verification: the application perspective, model-based testing and model inference, learning techniques for software verification and validation, LearnLib tutorial: from finite automata to register interface programs, RERS grey-box challenge 2012, Linux driver verification, bioscientific data processing and modeling, process and data integration in the networked healthcare, timing constraints: theory meets practice, formal methods for the development and certification of X-by-wire control systems, quantitative modelling and analysis, software aspects of robotic systems, process-oriented geoinformation systems and applications, handling heterogeneity in formal development of HW and SW Systems. Front Matter....Pages - Adaptable and Evolving Software for Eternal Systems....Pages 1-3 Challenges in Defining a Programming Language for Provably Correct Dynamic Analyses....Pages 4-18 Eternal Embedded Software: Towards Innovation Experiment Systems....Pages 19-31 A Liskov Principle for Delta-Oriented Programming....Pages 32-46 Scientific Workflows: Eternal Components, Changing Interfaces, Varying Compositions....Pages 47-63 An Object Group-Based Component Model....Pages 64-78 Automated Inference of Models for Black Box Systems Based on Interface Descriptions....Pages 79-96 Model-Based Compatibility Checking of System Modifications....Pages 97-111 A Generic Platform for Model-Based Regression Testing....Pages 112-126 Approaches for Mastering Change....Pages 127-130 A Formal Approach to Software Product Families....Pages 131-145 A Compositional Framework to Derive Product Line Behavioural Descriptions....Pages 146-161 Delta-Oriented Monitor Specification....Pages 162-177 Conflict Detection in Delta-Oriented Programming....Pages 178-192 Family-Based Analysis of Type Safety for Delta-Oriented Software Product Lines....Pages 193-207 A Vision for Behavioural Model-Driven Validation of Software Product Lines....Pages 208-222 Parameterized Preorder Relations for Model-Based Testing of Software Product Lines....Pages 223-237 SmartTies – Management of Safety-Critical Developments....Pages 238-252 Tracking Behavioral Constraints during Object-Oriented Software Evolution....Pages 253-268 Towards the Verification of Adaptable Processes....Pages 269-283 Runtime Verification: The Application Perspective....Pages 284-291 What Does AI Have to Do with RV?....Pages 292-294 A Case for “Piggyback” Runtime Monitoring....Pages 295-311 A Unified Approach for Static and Runtime Verification: Framework and Applications....Pages 312-326 Statistical Model Checking QoS Properties of Systems with SBIP....Pages 327-341 Monitoring Temporal Information Flow....Pages 342-357 Dynamic Information-Flow Analysis for Multi-threaded Applications....Pages 358-371 Bounded-Interference Sequentialization for Testing Concurrent Programs....Pages 372-387 Runtime Verification of Biological Systems....Pages 388-404 Behavioral Specification Based Runtime Monitors for OSGi Services....Pages 405-419 Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids....Pages 420-439 Model-Based Testing and Model Inference....Pages 440-443 Algorithmic Improvements on Regular Inference of Software Models and Perspectives for Security Testing....Pages 444-457 Test-Case Design by Feature Trees....Pages 458-473 Model-Based Static Code Analysis for MATLAB Models....Pages 474-487 An Incremental Learning Algorithm for Extended Mealy Automata....Pages 488-504 Learning Techniques for Software Verification and Validation....Pages 505-507 Learning Stochastic Timed Automata from Sample Executions....Pages 508-523 Learning Minimal Deterministic Automata from Inexperienced Teachers....Pages 524-538 Model Learning and Test Generation for Event-B Decomposition....Pages 539-553 Inferring Semantic Interfaces of Data Structures....Pages 554-571 Learning-Based Test Programming for Programmers....Pages 572-586 LearnLib Tutorial: From Finite Automata to Register Interface Programs....Pages 587-590 Automated Learning Setups in Automata Learning....Pages 591-607 The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems....Pages 608-614 Back Matter....Pages - Annotation The two-volume set LNCS 7609 and 7610 constitutes the thoroughly refereed proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, held in Heraklion, Crete, Greece, in October 2012. The two volumes contain papers presented in the topical sections on adaptable and evolving software for eternal systems, approaches for mastering change, runtime verification: the application perspective, model-based testing and model inference, learning techniques for software verification and validation, LearnLib tutorial: from finite automata to register interface programs, RERS grey-box challenge 2012, Linux driver verification, bioscientific data processing and modeling, process and data integration in the networked healthcare, timing constraints: theory meets practice, formal methods for the developent and certification of X-by-wire control systems, quantitative modelling and analysis, software aspects of robotic systems, process-oriented geoinformation systems and applications, handling heterogeneity in formal development of HW and SW Systems