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

✍ Scribed by Alessandro Moschitti (auth.), Tiziana Margaria, Bernhard Steffen (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2010
• Tongue: English
• Leaves: 517
• Series: Lecture Notes in Computer Science 6416 : Theoretical Computer Science and General Issues
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

Front Matter....Pages -
Introduction to the EternalS Track: Trustworthy Eternal Systems via Evolving Software, Data and Knowledge....Pages 1-2
HATS: Highly Adaptable and Trustworthy Software Using Formal Methods....Pages 3-8
SecureChange: Security Engineering for Lifelong Evolvable Systems....Pages 9-12
3DLife: Bringing the Media Internet to Life....Pages 13-14
LivingKnowledge: Kernel Methods for Relational Learning and Semantic Modeling....Pages 15-19
Task Forces in the EternalS Coordination Action....Pages 20-22
Modeling and Analyzing Diversity....Pages 23-25
Modeling and Managing System Evolution....Pages 26-29
Self-adaptation and Evolution by Learning....Pages 30-31
Overview of Roadmapping by EternalS....Pages 32-34
Adaptive Composition of Conversational Services through Graph Planning Encoding....Pages 35-50
Performance Prediction of Service-Oriented Systems with Layered Queueing Networks....Pages 51-65
Error Handling: From Theory to Practice....Pages 66-81
Modeling and Reasoning about Service Behaviors and Their Compositions....Pages 82-96
Design and Verification of Systems with Exogenous Coordination Using Vereofy....Pages 97-111
A Case Study in Model-Based Adaptation of Web Services....Pages 112-126
Quantitative Verification in Practice....Pages 127-127
Ten Years of Performance Evaluation for Concurrent Systems Using CADP....Pages 128-142
Towards Dynamic Adaptation of Probabilistic Systems....Pages 143-159
UPPAAL in Practice: Quantitative Verification of a RapidIO Network....Pages 160-174
Schedulability Analysis Using Uppaal: Herschel-Planck Case Study....Pages 175-190
Model-Checking Temporal Properties of Real-Time HTL Programs....Pages 191-205
Towards an Architecture for Runtime Interoperability....Pages 206-220
On Handling Data in Automata Learning....Pages 221-235
A Theory of Mediators for Eternal Connectors....Pages 236-250
On-the-Fly Interoperability through Automated Mediator Synthesis and Monitoring....Pages 251-262
Dependability Analysis and Verification for Connect ed Systems....Pages 263-277
Towards a Connector Algebra....Pages 278-292
Certification of Software-Driven Medical Devices....Pages 293-295
Arguing for Software Quality in an IEC 62304 Compliant Development Process....Pages 296-311
Trustable Formal Specification for Software Certification....Pages 312-326
Design Choices for High-Confidence Distributed Real-Time Software....Pages 327-342
Assurance Cases in Model-Driven Development of the Pacemaker Software....Pages 343-356
Improving Portability of Linux Applications by Early Detection of Interoperability Issues....Pages 357-370
Specification Based Conformance Testing for Email Protocols....Pages 371-381
Covering Arrays Generation Methods Survey....Pages 382-396
A Scalable Approach for the Description of Dependencies in Hard Real-Time Systems....Pages 397-411
Verification of Printer Datapaths Using Timed Automata....Pages 412-423
Resource Analysis of Automotive/Infotainment Systems Based on Domain-Specific Models – A Real-World Example....Pages 424-433
Source-Level Support for Timing Analysis....Pages 434-448
Practical Experiences of Applying Source-Level WCET Flow Analysis on Industrial Code....Pages 449-463
Worst-Case Analysis of Heap Allocations....Pages 464-478
Partial Flow Analysis with oRange....Pages 479-482
Towards an Evaluation Infrastructure for Automotive Multicore Real-Time Operating Systems....Pages 483-486
Context-Sensitivity in IPET for Measurement-Based Timing Analysis....Pages 487-490
On the Role of Non-functional Properties in Compiler Verification....Pages 491-495
Back Matter....Pages -

✦ Subjects

Logics and Meanings of Programs; Software Engineering; Programming Languages, Compilers, Interpreters; Computer Communication Networks; Information Systems Applications (incl.Internet); Data Mining and Knowledge Discovery