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.
Author(s): Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Helmut Veith (auth.), Tiziana Margaria, Bernhard Steffen (eds.)
Series: Lecture Notes in Computer Science 6415 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 708
Tags: Logics and Meanings of Programs; Software Engineering; Programming Languages, Compilers, Interpreters; Computer Communication Networks; Information Systems Applications (incl.Internet); Data Mining and Knowledge Discovery
Front Matter....Pages -
New Challenges in the Development of Critical Embedded Systems—An “aeromotive” Perspective....Pages 1-2
Certification of Embedded Software – Impact of ISO DIS 26262 in the Automotive Domain....Pages 3-3
Enforcing Applicability of Real-Time Scheduling Theory Feasibility Tests with the Use of Design-Patterns....Pages 4-17
Seamless Model-Driven Development Put into Practice....Pages 18-32
Timely Time Estimates....Pages 33-46
Compiler-Support for Robust Multi-core Computing....Pages 47-57
Thematic Track: Formal Languages and Methods for Designing and Verifying Complex Embedded Systems....Pages 58-59
Analyzing the Security in the GSM Radio Network Using Attack Jungles....Pages 60-74
Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method....Pages 75-89
Model-Driven Design-Space Exploration for Embedded Systems: The Octopus Toolset....Pages 90-105
Contract-Based Slicing....Pages 106-120
Special Track on Worst Case Traversal Time (WCTT)....Pages 121-121
The PEGASE Project: Precise and Scalable Temporal Analysis for Aerospace Communication Systems with Network Calculus....Pages 122-136
NC-Maude: A Rewriting Tool to Play with Network Calculus....Pages 137-151
DEBORAH: A Tool for Worst-Case Analysis of FIFO Tandems....Pages 152-168
A Self-adversarial Approach to Delay Analysis under Arbitrary Scheduling....Pages 169-183
Flow Control with (Min,+) Algebra....Pages 184-197
An Interface Algebra for Estimating Worst-Case Traversal Times in Component Networks....Pages 198-213
Towards Resource-Optimal Routing Plans for Real-Time Traffic....Pages 214-227
Partially Synchronizing Periodic Flows with Offsets Improves Worst-Case End-to-End Delay Analysis of Switched Ethernet....Pages 228-242
Analyzing End-to-End Functional Delays on an IMA Platform....Pages 243-257
Tools in Scientific Workflow Composition....Pages 258-260
Workflows for Metabolic Flux Analysis: Data Integration and Human Interaction....Pages 261-275
Intelligent Document Routing as a First Step towards Workflow Automation: A Case Study Implemented in SQL....Pages 276-284
Combining Subgroup Discovery and Permutation Testing to Reduce Reduncancy....Pages 285-300
Semantically-Guided Workflow Construction in Taverna: The SADI and BioMoby Plug-Ins....Pages 301-312
Workflow Construction for Service-Oriented Knowledge Discovery....Pages 313-327
Workflow Composition and Enactment Using jORCA....Pages 328-339
A Linked Data Approach to Sharing Workflows and Workflow Results....Pages 340-354
Towards More Adaptive Voice Applications....Pages 355-366
Telco Service Delivery Platforms in the Last Decade - A R&D Perspective....Pages 367-374
Ontology-Driven Pervasive Service Composition for Everyday Life....Pages 375-389
Navigating the Web of Things: Visualizing and Interacting with Web-Enabled Objects....Pages 390-398
Shaping Future Service Environments with the Cloud and Internet of Things: Networking Challenges and Service Evolution....Pages 399-410
Relay Placement Problem in Smart Grid Deployment....Pages 411-424
Towards a Research Agenda for Enterprise Crowdsourcing....Pages 425-434
Analyzing Collaboration in Software Development Processes through Social Networks....Pages 435-446
A Web-Based Framework for Collaborative Innovation....Pages 447-461
A Distributed Dynamics for WebGraph Decontamination....Pages 462-472
Increasing Users’ Trust on Personal Assistance Software Using a Domain-Neutral High-Level User Model....Pages 473-487
Understanding IT Organizations....Pages 488-501
On the 2-Categorical View of Proofs....Pages 502-518
WOMM: A Weak Operational Memory Model....Pages 519-534
A Memory Model for Static Analysis of C Programs....Pages 535-548
Analysing Message Sequence Graph Specifications....Pages 549-563
Optimize Context-Sensitive Andersen-Style Points-To Analysis by Method Summarization and Cycle-Elimination....Pages 564-578
A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL....Pages 579-593
SPARDL: A Requirement Modeling Language for Periodic Control System....Pages 594-608
AutoPA: Automatic Prototyping from Requirements....Pages 609-624
Systematic Model-Based Safety Assessment Via Probabilistic Model Checking....Pages 625-639
Learning Techniques for Software Verification and Validation – Special Track at ISoLA 2010....Pages 640-642
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning....Pages 643-657
Inferring Compact Models of Communication Protocol Entities....Pages 658-672
Inference and Abstraction of the Biometric Passport....Pages 673-686
From ZULU to RERS....Pages 687-704
Back Matter....Pages -
