LEADER 07466nam 22008055 450 001 996465956503316 005 20200706060700.0 010 $a1-280-39028-X 010 $a9786613568205 010 $a3-642-16901-5 024 7 $a10.1007/978-3-642-16901-4 035 $a(CKB)2670000000056662 035 $a(SSID)ssj0000446471 035 $a(PQKBManifestationID)11318129 035 $a(PQKBTitleCode)TC0000446471 035 $a(PQKBWorkID)10497336 035 $a(PQKB)11181001 035 $a(DE-He213)978-3-642-16901-4 035 $a(MiAaPQ)EBC3066104 035 $a(PPN)149890435 035 $a(EXLCZ)992670000000056662 100 $a20101108d2010 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFormal Methods and Software Engineering$b[electronic resource] $e12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings /$fedited by Jin Song Dong, Huibiao Zhu 205 $a1st ed. 2010. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010. 215 $a1 online resource (XIV, 712 p. 202 illus.) 225 1 $aProgramming and Software Engineering ;$v6447 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-16900-7 320 $aIncludes bibliographical references. 327 $aInvited Talks -- Fostering Proof Scores in CafeOBJ -- Exploiting Partial Success in Applying Automated Formal Methods -- Multicore Embedded Systems: The Timing Problem and Possible Solutions -- Theorem Proving and Decision Procedures -- Applying PVS Background Theories and Proof Strategies in Invariant Based Programming -- Proof Obligation Generation and Discharging for Recursive Definitions in VDM -- Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq -- Decision Procedures for the Temporal Verification of Concurrent Lists -- An Improved Decision Procedure for Propositional Projection Temporal Logic -- Web Services and Workflow -- A Semantic Model for Service Composition with Coordination Time Delays -- Compensable WorkFlow Nets -- Automatically Testing Web Services Choreography with Assertions -- Applying Ordinary Differential Equations to the Performance Analysis of Service Composition -- Verification I -- Verifying Heap-Manipulating Programs with Unknown Procedure Calls -- API Conformance Verification for Java Programs -- Assume-Guarantee Reasoning with Local Specifications -- Automating Coinduction with Case Analysis -- Applications of Formal Methods -- Enhanced Semantic Access to Formal Software Models -- Making Pattern- and Model-Based Software Development More Rigorous -- Practical Parameterised Session Types -- A Formal Verification Study on the Rotterdam Storm Surge Barrier -- Verification II -- Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems -- Automated Multiparameterised Verification by Cut-Offs -- Automating Cut-off for Multi-parameterized Systems -- Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors -- Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP -- Probability and Concurrency -- Model Checking Hierarchical Probabilistic Systems -- Trace-Driven Verification of Multithreaded Programs -- Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network -- Reasoning about Safety and Progress Using Contracts -- Program Analysis -- Abstract Program Slicing: From Theory towards an Implementation -- Loop Invariant Synthesis in a Combined Domain -- Software Metrics in Static Program Analysis -- A Combination of Forward and Backward Reachability Analysis Methods -- Model Checking -- Model Checking a Model Checker: A Code Contract Combined Approach -- On Symmetries and Spotlights ? Verifying Parameterised Systems -- A Methodology for Automatic Diagnosability Analysis -- Making the Right Cut in Model Checking Data-Intensive Timed Systems -- Comparison of Model Checking Tools for Information Systems -- Object Orientation and Model Driven Engineering -- A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model -- Model-Driven Protocol Design Based on Component Oriented Modeling -- Laws of Pattern Composition -- Dynamic Resource Reallocation between Deployment Components -- Specification and Verification -- A Pattern System to Support Refining Informal Ideas into Formal Expressions -- Specification Translation of State Machines from Equational Theories into Rewrite Theories -- Alternating Interval Based Temporal Logics. 330 $aThis book constitutes the refereed proceedings of the 12th International Conference on Formal Engineering Methods, ICFEM 2010, held in Shanghai, China, November 2010. The 42 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 114 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on theorem proving and decision procedures, web services and workflow, verification, applications of formal methods, probability and concurrency, program analysis, model checking, object orientation and mod el driven engineering, as well as specification and verification. 410 0$aProgramming and Software Engineering ;$v6447 606 $aSoftware engineering 606 $aComputer communication systems 606 $aProgramming languages (Electronic computers) 606 $aComputer programming 606 $aAlgorithms 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aAlgorithm Analysis and Problem Complexity$3https://scigraph.springernature.com/ontologies/product-market-codes/I16021 607 $aSchanghai <2010>$2swd 608 $aKongress.$2swd 615 0$aSoftware engineering. 615 0$aComputer communication systems. 615 0$aProgramming languages (Electronic computers). 615 0$aComputer programming. 615 0$aAlgorithms. 615 14$aSoftware Engineering/Programming and Operating Systems. 615 24$aComputer Communication Networks. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aSoftware Engineering. 615 24$aProgramming Techniques. 615 24$aAlgorithm Analysis and Problem Complexity. 676 $a005.1 702 $aDong$b Jin Song$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aZhu$b Huibiao$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Formal Engineering Methods 906 $aBOOK 912 $a996465956503316 996 $aFormal Methods and Software Engineering$9771999 997 $aUNISA