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.
Author(s): Kokichi Futatsugi (auth.), Jin Song Dong, Huibiao Zhu (eds.)
Series: Lecture Notes in Computer Science 6447 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 712
Tags: Software Engineering; Programming Techniques; Programming Languages, Compilers, Interpreters; Algorithm Analysis and Problem Complexity; Mathematical Logic and Formal Languages; Computer Communication Networks
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 -
