Formal Methods and Software Engineering

This volume contains the proceedings of the Fourth International Conference on Formal Engineering Methods: ICFEM 2002. The conference was held in Sha- hai,China,from 21 to 25 October 2002. Formal methods for software development have been extensively researched and their use in industry is increasing. Recent applications to the development of safety-critical,security-critical,and mission-critical systems have signi?cantly increased trustworthiness,without increasing overall development costs. ICFEM encourages the exchange of ideas on recent advances in formal methods and software engineering. The conference received 108 papers submitted from 24 di?erent countries and regions. A total of 43 regular and 16 short papers were accepted. All papers were reviewed by three or four members of the program committee or other reviewers. The conference would not have been possible without their voluntary and dedicated work. The conference had a number of excellent keynote speakers: Prof. Ralph- Johan Back of Abo Akademi University,Finland,Dr. Mark A. Hale of Inter woven Inc.,USA,Dr. Richard J ullig of CommerceNet Consortium,USA,Prof. Shaoying Liu of Hosei University,Japan,and Prof. Jim Woodcock of the University of Kent,UK. They provided a balanced view of advanced formal methods and software engineering from their research programs and experience.

Includes supplementary material: sn.pub/extras

Inhalt
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.