Formal Methods and Software Engineering: 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings

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 -