Formal Methods and Software Engineering

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.