Formal Methods and Software Engineering : 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings

by Liu, Zhiming; He, Jifeng

• ISBN13: 9783540474609
• ISBN10: 3540474609
• Format: Paperback
• Copyright: 2007-01-03
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 8th International Conference on Formal Engineering Methods, ICFEM 2006, held in Macao, China, in November 2006. The 38 revised full papers presented together with 3 keynote talks were carefully reviewed and selected from 108 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on specification and verification, internetware and Web-based systems, concurrent, communicating, timing and probabilistic systems, object and component orientation, testing and model checking, tools, fault-tolerance and security, as well as specification and refinement.

Table of Contents

Keynote Talks
Program Verification Through Computer Algebra	p. 1
JML's Rich, Inherited Specifications for Behavioral Subtypes	p. 2
Three Perspectives in Formal Engineering	p. 35
Specification and Verification
A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces	p. 55
Applying Timed Interval Calculus to Simulink Diagrams	p. 74
Reducing Model Checking of the Few to the One	p. 94
Induction-Guided Falsification	p. 114
Verifying [chi] Models of Industrial Systems with Spin	p. 132
Stateful Dynamic Partial-Order Reduction	p. 149
Internetware and Web-Based Systems
User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition	p. 168
Environment Ontology-Based Capability Specification for Web Service Discovery	p. 185
Scenario-Based Component Behavior Derivation	p. 206
Verification of Computation Orchestration Via Timed Automata	p. 226
Towards the Semantics for Web Service Choreography Description Language	p. 246
Type Checking Choreography Description Language	p. 264
Concurrent, Communicating, Timing and Probabilistic Systems
Formalising Progress Properties of Non-blocking Programs	p. 284
Towards a Fully Generic Theory of Data	p. 304
Verifying Statemate Statecharts Using CSP and FDR	p. 324
A Reasoning Method for Timed CSP Based on Constraint Solving	p. 342
Mapping RT-LOTOS Specifications into Time Petri Nets	p. 360
Reasoning Algebraically About Probabilistic Loops	p. 380
Object and Component Orientation
Formal Verification of the Heap Manager of an Operating System Using Separation Logic	p. 400
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs	p. 420
Model Checking Dynamic UML Consistency	p. 440
Testing and Model Checking
Conditions for Avoiding Controllability Problems in Distributed Testing	p. 460
Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm	p. 478
Checking the Conformance of Java Classes Against Algebraic Specifications	p. 494
Incremental Slicing	p. 514
Assume-Guarantee Software Verification Based on Game Semantics	p. 529
Optimized Execution of Deterministic Blocks in Java PathFinder	p. 549
Tools
A Tool for a Formal Pattern Modeling Language	p. 568
An Open Extensible Tool Environment for Event-B	p. 588
Tool for Translating Simulink Models into Input Language of a Model Checker	p. 606
Fault-Tolerance and Security
Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices	p. 621
A Language for Modeling Network Availability	p. 639
Multi-process Systems Analysis Using Event B: Application to Group Communication Systems	p. 660
Specification and Refinement
Issues in Implementing a Model Checker for Z	p. 678
Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking	p. 697
Discovering Likely Method Specifications	p. 717
Time Aware Modelling and Analysis of Multiclocked VLSI Systems	p. 737
SALT-Structured Assertion Language for Temporal Logic	p. 757
Author Index	p. 777
Table of Contents provided by Ingram. All Rights Reserved.