| Invited Talks | |
| SFI: A Refinement Based Layered Software Architecture | p. 1 |
| Developing Quality Software Systems Using the SOFL Formal Engineering Method | p. 3 |
| Maintaining Referential Integrity on the Web | p. 20 |
| Formal Methods in Enterprise Computing | p. 22 |
| Unifying Theories of Parallel Programming | p. 24 |
| Component Engineering and Software Architecture | |
| ABC/ADL: An ADL Supporting Component Composition | p. 38 |
| The Description of CORBA Objects Based on Petri Nets | p. 48 |
| Toward a Formal Model of Software Components | p. 57 |
| A Specification-Based Software Construction Framework for Reuse | p. 69 |
| Specifying a Component Model for Building Dynamically Reconfigurable Distributed Systems | p. 80 |
| Three-Tiered Specification of Micro-architectures | p. 92 |
| Modeling the Architecture for Component-Based E-commerce System | p. 98 |
| Component Specification and Wrapper/Glue Code Generation with Two-Level Grammar Using Domain Specific Knowledge | p. 103 |
| Method Integration | |
| Abstract Specification in Object-Z and CSP | p. 108 |
| Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS | p. 120 |
| Specification Techniques and Languages | |
| Concept Use or Concept Refinement: An Important Distinction in Building Generic Specifications | p. 132 |
| An Overview of Mobile Object-Z | p. 144 |
| Z Approach to Semantic Web | p. 156 |
| Hardware/Software Partitioning in Verilog | p. 168 |
| A Formal Methodology to Specify E-commerce Systems | p. 180 |
| Model-Based Specification Animation Using Testgraphs | p. 192 |
| An Abstract Model for Scheduling Real-Time Programs | p. 204 |
| A Specification and Validation Technique Based on STATEMATE and FNLOG | p. 216 |
| Formal Representation and Analysis of Batch Stock Trading Systems by Logical Petri Net Workflows | p. 221 |
| A Calculus for Mobile Network Systems | p. 226 |
| Modelling Real-Time Systems with Continuous-Time Temporal Logic | p. 231 |
| On Concept-Based Definition of Domain-Specific Languages | p. 237 |
| Formal Specification of Evolutionary Software Agents | p. 249 |
| Detecting Deadlock in Ada Rendezvous Flow Structure Based on Process Algebra | p. 262 |
| Formal Analysis of Real-Time Systems with SAM | p. 275 |
| Tools and Environments | |
| Tool Support for Visualizing CSP in UML | p. 287 |
| Theorem Prover Support for Precondition and Correctness Calculation | p. 299 |
| XML-Based Static Type Checking and Dynamic Visualization for TCOZ | p. 311 |
| Refinement | |
| -Chart-Based Specification and Refinement | p. 323 |
| Towards a Refinement Calculus for Concurrent Real-Time Programs | p. 335 |
| Refinement Algebra for Formal Bytecode Generation | p. 347 |
| Applications | |
| Formal Modelling of Java GUI Event Handling | p. 359 |
| A New Algorithm for Service Interaction Detection | p. 371 |
| Specification of an Asynchronous On-chip Bus | p. 383 |
| Analysis of a Security Protocol in CRL | p. 396 |
| Developing a Spell-Checker for Tajik Using RAISE | p. 401 |
| M2Z: A Tool for Translating a Natural Language Software Specificationinto Z | p. 406 |
| Validation and Verification | |
| Abstract Interpretation with a Theorem Prover | p. 411 |
| Formal Reasoning about Hardware and Software Memory Models | p. 423 |
| Slicing Hierarchical Automata for Model Checking UML Statecharts | p. 435 |
| Formal Verification of a SONET Telecom System Block | p. 447 |
| Enabling Hardware Verification through Design Changes | p. 459 |
| Specification-Based Test Generation for Security-Critical Systems Using Mutations | p. 471 |
| A Formal Definition of Function Points for Automated Measurement of B Specifications | p. 483 |
| Machine Code Type Safety | p. 495 |
| UML | |
| On the Formalized Semantics of Static Modeling Elements in UML | p. 500 |
| From a B Specification to UML StateChart Diagrams | p. 511 |
| Formalizing UML Models with Object-Z | p. 523 |
| Using Transition Systems to Unify UML Models | p. 535 |
| A Formal Metamodeling Approach to a Transformation between the UML State Machine and Object-Z | p. 548 |
| A UML Approach to the Design of Open Distributed Systems | p. 561 |
| A Semantic Model of Real-Time UML | p. 573 |
| Research on Ontology-Oriented Domain Analysis on MIS | p. 578 |
| A Requirements Description Model Based on Conditional Directed Graphs | p. 583 |
| Semantics | |
| Introducing Reference Semantics via Refinement | p. 588 |
| Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational Semantics | p. 600 |
| Towards a Time Model for Circus | p. 613 |
| Author Index | p. 625 |
| Table of Contents provided by Publisher. All Rights Reserved. |
