Leveraging applications of formal methods, verification and validation : discussion, dissemination, applications : 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings. Part II

The two-volume set LNCS 9952 and LNCS 9953 constitutes the refereed proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, held in Imperial, Corfu, Greece, in October 2016. The papers presented in this volume were carefully reviewed and selected for inclusion in the proceedings. Featuring a track introduction to each section, the papers are organized in topical sections named: statistical model checking; evaluation and reproducibility of program analysis and verification; ModSyn-PP: modular synthesis of programs and processes; semantic heterogeneity in the formal development of complex systems; static and runtime verification: competitors or friends?; rigorous engineering of collective adaptive systems; correctness-by-construction and post-hoc verification: friends or foes?; privacy and security issues in information systems; towards a unified view of modeling and programming; formal methods and safety certification: challenges in the railways domain; RVE: runtime verification and enforcement, the (industrial) application perspective; variability modeling for scalable software evolution; detecting and understanding software doping; learning systems: machine-learning in software products and learning-based analysis of software systems; testing the internet of things; doctoral symposium; industrial track; RERS challenge; and STRESS. Front Matter....Pages I-XXIV Front Matter....Pages 1-1 Towards a Unified View of Modeling and Programming (Track Summary)....Pages 3-10 Programming ⊂ Modeling ⊂ Engineering....Pages 11-26 On a Unified View of Modeling and Programming Position Paper....Pages 27-31 On the Feasibility of a Unified Modelling and Programming Paradigm....Pages 32-49 Modeling Meets Programming: A Comparative Study in Model Driven Engineering Action Languages....Pages 50-67 Abstractions for Modeling Complex Systems....Pages 68-79 Specifying and Verifying Advanced Control Features....Pages 80-96 Simplifying OMG MOF-Based Metamodeling....Pages 97-118 Modelling and Testing of Real Systems....Pages 119-130 Unifying Modelling and Programming: A Systems Biology Perspective....Pages 131-133 Formally Unifying Modeling and Design for Embedded Systems - A Personal View....Pages 134-149 Interactive Model-Based Compilation Continued – Incremental Hardware Synthesis for SCCharts....Pages 150-170 Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design....Pages 171-186 Merging Modeling and Programming Using Umple....Pages 187-197 Systems Modeling and Programming in a Unified Environment Based on Julia....Pages 198-217 Meta-Level Reuse for Mastering Domain Specialization....Pages 218-237 Towards a Unified View of Modeling and Programming....Pages 238-257 Front Matter....Pages 259-259 Formal Methods and Safety Certification: Challenges in the Railways Domain....Pages 261-265 On the Use of Static Checking in the Verification of Interlocking Systems....Pages 266-278 Compositional Verification of Multi-station Interlocking Systems....Pages 279-293 Front Matter....Pages 259-259 OnTrack: The Railway Verification Toolset....Pages 294-296 Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a CBTC System....Pages 297-314 Tuning Energy Consumption Strategies in the Railway Domain: A Model-Based Approach....Pages 315-330 Front Matter....Pages 331-331 Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction)....Pages 333-338 What Is a Trace? A Runtime Verification Perspective....Pages 339-355 Challenges in Fault-Tolerant Distributed Runtime Verification....Pages 356-362 The HARMONIA Project: Hardware Monitoring for Automotive Systems-of-Systems....Pages 363-370 Runtime Verification for Interconnected Medical Devices....Pages 371-379 Dynamic Analysis of Regression Problems in Industrial Systems: Challenges and Solutions....Pages 380-387 Towards a Logic for Inferring Properties of Event Streams....Pages 388-393 Runtime Verification for Stream Processing Applications....Pages 394-399 On the Runtime Enforcement of Evolving Privacy Policies in Online Social Networks....Pages 400-406 On the Specification and Enforcement of Privacy-Preserving Contractual Agreements....Pages 407-412 Front Matter....Pages 413-419 Introduction to the Track on Variability Modeling for Scalable Software Evolution....Pages 421-421 Towards Incremental Validation of Railway Systems....Pages 423-432 Modeling and Optimizing Automotive Electric/Electronic (E/E) Architectures: Towards Making Clafer Accessible to Practitioners....Pages 433-446 Variability-Based Design of Services for Smart Transportation Systems....Pages 447-464 Comparing AWS Deployments Using Model-Based Predictions....Pages 465-481 A Toolchain for Delta-Oriented Modeling of Software Product Lines....Pages 482-496 Front Matter....Pages 497-511 A Technology-Neutral Role-Based Collaboration Model for Software Ecosystems....Pages 421-421 Adaptable Runtime Monitoring for the Java Virtual Machine....Pages 512-530 Identifying Variability in Object-Oriented Code Using Model-Based Code Mining....Pages 531-546 User Profiles for Context-Aware Reconfiguration in Software Product Lines....Pages 547-562 Refactoring Delta-Oriented Product Lines to Enforce Guidelines for Efficient Type-Checking....Pages 563-578 Front Matter....Pages 579-596 Facets of Software Doping....Pages 597-599 Software that Meets Its Intent....Pages 601-608 Compliance, Functional Safety and Fault Detection by Formal Methods....Pages 609-625 What the Hack Is Wrong with Software Doping?....Pages 626-632 Front Matter....Pages 633-647 Learning Systems: Machine-Learning in Software Products and Learning-Based Analysis of Software Systems....Pages 649-649 ALEX: Mixed-Mode Learning of Web Applications at Ease....Pages 651-654 Assuring the Safety of Advanced Driver Assistance Systems Through a Combination of Simulation and Runtime Monitoring....Pages 655-671 Enhancement of an Adaptive HEV Operating Strategy Using Machine Learning Algorithms....Pages 672-687 Front Matter....Pages 688-702 Data Science Challenges to Improve Quality Assurance of Internet of Things Applications....Pages 703-706 Model-Based Testing as a Service for IoT Platforms....Pages 707-726 Front Matter....Pages 727-742 Handling Domain Knowledge in Formal Design Models: An Ontology Based Approach....Pages 743-745 Front Matter....Pages 747-751 Effective and Efficient Customization Through Lean Trans-Departmental Configuration....Pages 753-755 A Fully Model-Based Approach to Software Development for Industrial Centrifuges....Pages 757-773 Front Matter....Pages 774-783 RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification....Pages 785-785 Front Matter....Pages 787-803 DIME: A Programming-Less Modeling Environment for Web Applications....Pages 805-807 Front Matter....Pages 809-832 Verification Techniques for Hybrid Systems....Pages 805-807 On the Power of Statistical Model Checking....Pages 833-842 Back Matter....Pages 843-862 ....Pages 863-866