Formal Methods and Software Engineering 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, October 21-25, 2002, Proceedings

This book constitutes the refereed proceedings of the 4th International Conference on Formal Engineering methods, ICFEM 2002, held in Shanghai, China, in October 2002.
The 43 revised full papers and 16 revised short papers presented together with 5 invited contributions were carefully reviewed and selected from a total of 108 submissions. The papers are organized in topical sections on component engineering and software architecture, method integration, specification techniques and languages, tools and environments, refinement, applications, validation and verification, UML, and semantics.

Invited Talks.- SFI: A Refinement Based Layered Software Architecture.- Developing Quality Software Systems Using the SOFL Formal Engineering Method.- Maintaining Referential Integrity on the Web.- Formal Methods in Enterprise Computing.- Unifying Theories of Parallel Programming.- Component Engineering and Software Architecture.- ABC/ADL: An ADL Supporting Component Composition.- The Description of CORBA Objects Based on Petri Nets.- Toward a Formal Model of Software Components.- A Specification-Based Software Construction Framework for Reuse.- Specifying a Component Model for Building Dynamically Reconfigurable Distributed Systems.- Three-Tiered Specification of Micro-architectures.- Modeling the Architecture for Component-Based E-commerce System.- Component Specification and Wrapper/Glue Code Generation with Two-Level Grammar Using Domain Specific Knowledge.- Method Integration.- Abstract Specification in Object-Z and CSP.- Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS.- Specification Techniques and Languages.- Concept Use or Concept Refinement: An Important Distinction in Building Generic Specifications.- An Overview of Mobile Object-Z.- Z Approach to Semantic Web.- Hardware/Software Partitioning in Verilog.- A Formal Methodology to Specify E-commerce Systems.- Model-Based Specification Animation Using Testgraphs.- An Abstract Model for Scheduling Real-Time Programs.- A Specification and Validation Technique Based on STATEMATE and FNLOG.- Formal Representation and Analysis of Batch Stock Trading Systems by Logical Petri Net Workflows.- A Calculus for Mobile Network Systems.- Modelling Real-Time Systems with Continuous-Time Temporal Logic.- On Concept-Based Definition of Domain-Specific Languages.- Formal Specification of Evolutionary Software Agents.- Detecting Deadlock in Ada Rendezvous Flow Structure Based on Process Algebra.- Formal Analysis of Real-Time Systems with SAM.- Tools and Environments.- Tool Support for Visualizing CSP in UML.- Theorem Prover Support for Precondition and Correctness Calculation.- XML-Based Static Type Checking and Dynamic Visualization for TCOZ.- Refinement.- ?-Chart-Based Specification and Refinement.- Towards a Refinement Calculus for Concurrent Real-Time Programs.- Refinement Algebra for Formal Bytecode Generation.- Applications.- Formal Modelling of Java GUI Event Handling.- A New Algorithm for Service Interaction Detection.- Specification of an Asynchronous On-chip Bus.- Analysis of a Security Protocol in ?CRL.- Developing a Spell-Checker for Tajik Using RAISE.- M2Z: A Tool for Translating a Natural Language Software Specification into Z.- Validation and Verification.- Abstract Interpretation with a Theorem Prover.- Formal Reasoning about Hardware and Software Memory Models.- Slicing Hierarchical Automata for Model Checking UML Statecharts.- Formal Verification of a SONET Telecom System Block.- Enabling Hardware Verification through Design Changes.- Specification-Based Test Generation for Security-Critical Systems Using Mutations.- A Formal Definition of Function Points for Automated Measurement of B Specifications.- Machine Code Type Safety.- UML.- On the Formalized Semantics of Static Modeling Elements in UML.- From a B Specification to UML StateChart Diagrams.- Formalizing UML Models with Object-Z.- Using Transition Systems to Unify UML Models.- A Formal Metamodeling Approach to a Transformation between the UML State Machine and Object-Z.- A UML Approach to the Design of Open Distributed Systems.- A Semantic Model of Real-Time UML.- Research on Ontology-OrientedDomain Analysiss on MIS.- A Requirements Description Model Based on Conditional Directed Graphs.- Semantics.- Introducing Reference Semantics via Refinement.- Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational Semantics.- Towards a Time Model for Circus.