Formal methods and software engineering : 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010 ; proceedings

This 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 model driven engineering, as well as specification and verification. Front Matter....Pages - Fostering Proof Scores in CafeOBJ ....Pages 1-20 Exploiting Partial Success in Applying Automated Formal Methods....Pages 21-21 Multicore Embedded Systems: The Timing Problem and Possible Solutions....Pages 22-23 Applying PVS Background Theories and Proof Strategies in Invariant Based Programming....Pages 24-39 Proof Obligation Generation and Discharging for Recursive Definitions in VDM....Pages 40-55 Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq....Pages 56-73 Decision Procedures for the Temporal Verification of Concurrent Lists....Pages 74-89 An Improved Decision Procedure for Propositional Projection Temporal Logic....Pages 90-105 A Semantic Model for Service Composition with Coordination Time Delays....Pages 106-121 Compensable WorkFlow Nets....Pages 122-137 Automatically Testing Web Services Choreography with Assertions....Pages 138-154 Applying Ordinary Differential Equations to the Performance Analysis of Service Composition....Pages 155-170 Verifying Heap-Manipulating Programs with Unknown Procedure Calls....Pages 171-187 API Conformance Verification for Java Programs....Pages 188-203 Assume-Guarantee Reasoning with Local Specifications....Pages 204-219 Automating Coinduction with Case Analysis....Pages 220-236 Enhanced Semantic Access to Formal Software Models....Pages 237-252 Making Pattern- and Model-Based Software Development More Rigorous....Pages 253-269 Practical Parameterised Session Types....Pages 270-286 A Formal Verification Study on the Rotterdam Storm Surge Barrier....Pages 287-302 Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems....Pages 303-320 Automated Multiparameterised Verification by Cut-Offs....Pages 321-337 Automating Cut-off for Multi-parameterized Systems....Pages 338-354 Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors....Pages 355-370 Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP....Pages 371-387 Model Checking Hierarchical Probabilistic Systems....Pages 388-403 Trace-Driven Verification of Multithreaded Programs....Pages 404-419 Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network....Pages 420-435 Reasoning about Safety and Progress Using Contracts....Pages 436-451 Abstract Program Slicing: From Theory towards an Implementation....Pages 452-467 Loop Invariant Synthesis in a Combined Domain....Pages 468-484 Software Metrics in Static Program Analysis....Pages 485-500 A Combination of Forward and Backward Reachability Analysis Methods....Pages 501-517 Model Checking a Model Checker: A Code Contract Combined Approach....Pages 518-533 On Symmetries and Spotlights – Verifying Parameterised Systems....Pages 534-548 A Methodology for Automatic Diagnosability Analysis....Pages 549-564 Making the Right Cut in Model Checking Data-Intensive Timed Systems....Pages 565-580 Comparison of Model Checking Tools for Information Systems....Pages 581-596 A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model....Pages 597-612 Model-Driven Protocol Design Based on Component Oriented Modeling....Pages 613-629 Laws of Pattern Composition....Pages 630-645 Dynamic Resource Reallocation between Deployment Components....Pages 646-661 A Pattern System to Support Refining Informal Ideas into Formal Expressions....Pages 662-677 Specification Translation of State Machines from Equational Theories into Rewrite Theories....Pages 678-693 Alternating Interval Based Temporal Logics....Pages 694-709 Back Matter....Pages - Annotation This book constitutes the refereed proceedings of the 12th InternationalConference 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 model driven engineering, as well as specification and verification. This 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