LEADER 07810nam 22008415 450 001 9910483513703321 005 20251226200244.0 010 $a1-280-39006-9 010 $a9786613567987 010 $a3-642-16561-3 024 7 $a10.1007/978-3-642-16561-0 035 $a(CKB)2670000000056647 035 $a(SSID)ssj0000446595 035 $a(PQKBManifestationID)11291907 035 $a(PQKBTitleCode)TC0000446595 035 $a(PQKBWorkID)10497082 035 $a(PQKB)10307907 035 $a(DE-He213)978-3-642-16561-0 035 $a(MiAaPQ)EBC3066051 035 $a(PPN)149890745 035 $a(BIP)32335641 035 $a(EXLCZ)992670000000056647 100 $a20101102d2010 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aLeveraging Applications of Formal Methods, Verification, and Validation $e4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II /$fedited by Tiziana Margaria, Bernhard Steffen 205 $a1st ed. 2010. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010. 215 $a1 online resource (XV, 498 p. 157 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6416 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-642-16560-5 320 $aIncludes bibliographical references and index. 327 $aEternalS: Mission and Roadmap -- to the EternalS Track: Trustworthy Eternal Systems via Evolving Software, Data and Knowledge -- HATS: Highly Adaptable and Trustworthy Software Using Formal Methods -- SecureChange: Security Engineering for Lifelong Evolvable Systems -- 3DLife: Bringing the Media Internet to Life -- LivingKnowledge: Kernel Methods for Relational Learning and Semantic Modeling -- Task Forces in the EternalS Coordination Action -- Modeling and Analyzing Diversity -- Modeling and Managing System Evolution -- Self-adaptation and Evolution by Learning -- Overview of Roadmapping by EternalS -- Formal Methods in Model-Driven Development for Service-Oriented and Cloud Computing -- Adaptive Composition of Conversational Services through Graph Planning Encoding -- Performance Prediction of Service-Oriented Systems with Layered Queueing Networks -- Error Handling: From Theory to Practice -- Modeling and Reasoning about Service Behaviors and Their Compositions -- Design and Verification of Systems with Exogenous Coordination Using Vereofy -- A Case Study in Model-Based Adaptation of Web Services -- Quantitative Verification in Practice -- Quantitative Verification in Practice -- Ten Years of Performance Evaluation for Concurrent Systems Using CADP -- Towards Dynamic Adaptation of Probabilistic Systems -- UPPAAL in Practice: Quantitative Verification of a RapidIO Network -- Schedulability Analysis Using Uppaal: Herschel-Planck Case Study -- Model-Checking Temporal Properties of Real-Time HTL Programs -- CONNECT: Status and Plans -- Towards an Architecture for Runtime Interoperability -- On Handling Data in Automata Learning -- A Theory of Mediators for Eternal Connectors -- On-the-Fly Interoperability through Automated Mediator Synthesis and Monitoring -- Dependability Analysis and Verification for Connected Systems -- Towards a Connector Algebra -- Certification of Software-Driven Medical Devices -- Certification of Software-Driven Medical Devices -- Arguing for Software Quality in an IEC 62304 Compliant Development Process -- Trustable Formal Specification for Software Certification -- Design Choices for High-Confidence Distributed Real-Time Software -- Assurance Cases in Model-Driven Development of the Pacemaker Software -- Modeling and Formalizing Industrial Software for Verification, Validation and Certification -- Improving Portability of Linux Applications by Early Detection of Interoperability Issues -- Specification Based Conformance Testing for Email Protocols -- Covering Arrays Generation Methods Survey -- Resource and Timing Analysis -- A Scalable Approach for the Description of Dependencies in Hard Real-Time Systems -- Verification of Printer Datapaths Using Timed Automata -- Resource Analysis of Automotive/Infotainment Systems Based on Domain-Specific Models ? A Real-World Example -- Source-Level Support for Timing Analysis -- Practical Experiences of Applying Source-Level WCET Flow Analysis on Industrial Code -- Worst-Case Analysis of Heap Allocations -- Partial Flow Analysis with oRange -- Towards an Evaluation Infrastructure for Automotive Multicore Real-Time Operating Systems -- Context-Sensitivity in IPET for Measurement-Based Timing Analysis -- On the Role of Non-functional Properties in Compiler Verification. 330 $aThis volume contains the conference proceedings of the 4th International S- posium on Leveraging Applications of Formal Methods, Veri'cation and Vali- tion, ISoLA 2010, which was held in Greece (Heraklion, Crete) October 18-21, 2010, and sponsored by EASST. Following the tradition of its forerunners in 2004, 2006, and 2008 in Cyprus and Chalchidiki, and the ISoLA Workshops in Greenbelt (USA) in 2005, in Poitiers (France) in 2007, and in Potsdam (Germany) in 2009, ISoLA 2010 p- vided a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools and methods for the speci'cation, ana- sis, veri'cation, certi'cation, construction, testing, and maintenance of systems from the point of view of their di'erent application domains. Thus, the ISoLA series of events serves the purpose of bridging the gap between designers and developers of rigorous tools, and users in engineering and in other disciplines, and to foster and exploit synergetic relationships among scientists, engineers, software developers, decision makers, and other critical thinkers in companies and organizations. In particular, by providing a venue for the discussion of c- mon problems, requirements, algorithms, methodologies, and practices, ISoLA aims at supporting researchers in their quest to improve the utility, reliability, ?exibility, and e'ciency of tools for building systems, and users in their search for adequate solutions to their problems. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6416 606 $aComputer networks 606 $aComputer science 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aApplication software 606 $aData mining 606 $aComputer Communication Networks 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aComputer and Information Systems Applications 606 $aData Mining and Knowledge Discovery 615 0$aComputer networks. 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aApplication software. 615 0$aData mining. 615 14$aComputer Communication Networks. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aComputer and Information Systems Applications. 615 24$aData Mining and Knowledge Discovery. 676 $a004.6 701 $aMargaria-Steffen$b Tiziana$f1964-$0845731 701 $aSteffens$b Bernhard$01752536 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483513703321 996 $aLeveraging applications of formal methods, verification, and validation$94187854 997 $aUNINA