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-Oriented Domain 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.