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

✍ Scribed by Ralph-Johan Back (auth.), Chris George, Huaikou Miao (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2002
• Tongue: English
• Leaves: 638
• Series: Lecture Notes in Computer Science 2495
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

SFI: A Refinement Based Layered Software Architecture....Pages 1-2
Developing Quality Software Systems Using the SOFL Formal Engineering Method....Pages 3-19
Maintaining Referential Integrity on the Web....Pages 20-21
Formal Methods in Enterprise Computing....Pages 22-23
Unifying Theories of Parallel Programming....Pages 24-37
ABC/ADL: An ADL Supporting Component Composition....Pages 38-47
The Description of CORBA Objects Based on Petri Nets....Pages 48-56
Toward a Formal Model of Software Components....Pages 57-68
A Specification-Based Software Construction Framework for Reuse....Pages 69-79
Specifying a Component Model for Building Dynamically Reconfigurable Distributed Systems....Pages 80-91
Three-Tiered Specification of Micro-architectures....Pages 92-97
Modeling the Architecture for Component-Based E-commerce System....Pages 98-102
Component Specification and Wrapper/Glue Code Generation with Two-Level Grammar Using Domain Specific Knowledge....Pages 103-107
Abstract Specification in Object-Z and CSP....Pages 108-119
Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS....Pages 120-131
Concept Use or Concept Refinement: An Important Distinction in Building Generic Specifications....Pages 132-143
An Overview of Mobile Object-Z....Pages 144-155
Z Approach to Semantic Web....Pages 156-167
Hardware/Software Partitioning in Verilog....Pages 168-179
A Formal Methodology to Specify E-commerce Systems....Pages 180-191
Model-Based Specification Animation Using Testgraphs....Pages 192-203
An Abstract Model for Scheduling Real-Time Programs....Pages 204-215
A Specification and Validation Technique Based on STATEMATE and FNLOG....Pages 216-220
Formal Representation and Analysis of Batch Stock Trading Systems by Logical Petri Net Workflows....Pages 221-225
A Calculus for Mobile Network Systems....Pages 226-230
Modelling Real-Time Systems with Continuous-Time Temporal Logic....Pages 231-236
On Concept-Based Definition of Domain-Specific Languages....Pages 237-248
Formal Specification of Evolutionary Software Agents....Pages 249-261
Detecting Deadlock in Ada Rendezvous Flow Structure Based on Process Algebra....Pages 262-274
Formal Analysis of Real-Time Systems with SAM....Pages 275-286
Tool Support for Visualizing CSP in UML....Pages 287-298
Theorem Prover Support for Precondition and Correctness Calculation....Pages 299-310
XML-Based Static Type Checking and Dynamic Visualization for TCOZ....Pages 311-322
μ-Chart-Based Specification and Refinement....Pages 323-334
Towards a Refinement Calculus for Concurrent Real-Time Programs....Pages 335-347
Refinement Algebra for Formal Bytecode Generation....Pages 347-358
Formal Modelling of Java GUI Event Handling....Pages 359-370
A New Algorithm for Service Interaction Detection....Pages 371-382
Specification of an Asynchronous On-chip Bus....Pages 383-395
Analysis of a Security Protocol in μCRL....Pages 396-400
Developing a Spell-Checker for Tajik Using RAISE....Pages 401-405
M2Z: A Tool for Translating a Natural Language Software Specification into Z....Pages 406-410
Abstract Interpretation with a Theorem Prover....Pages 411-422
Formal Reasoning about Hardware and Software Memory Models....Pages 423-434
Slicing Hierarchical Automata for Model Checking UML Statecharts....Pages 435-446
Formal Verification of a SONET Telecom System Block....Pages 447-458
Enabling Hardware Verification through Design Changes....Pages 459-470
Specification-Based Test Generation for Security-Critical Systems Using Mutations....Pages 471-482
A Formal Definition of Function Points for Automated Measurement of B Specifications....Pages 483-494
Machine Code Type Safety....Pages 495-499
On the Formalized Semantics of Static Modeling Elements in UML....Pages 500-510
From a B Specification to UML StateChart Diagrams....Pages 511-522
Formalizing UML Models with Object-Z....Pages 523-534
Using Transition Systems to Unify UML Models....Pages 535-547
A Formal Metamodeling Approach to a Transformation between the UML State Machine and Object-Z....Pages 548-560
A UML Approach to the Design of Open Distributed Systems....Pages 561-572
A Semantic Model of Real-Time UML....Pages 573-577
Research on Ontology-Oriented Domain Analysiss on MIS....Pages 578-582
A Requirements Description Model Based on Conditional Directed Graphs....Pages 583-587
Introducing Reference Semantics via Refinement....Pages 588-599
Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational Semantics....Pages 600-612
Towards a Time Model for Circus ....Pages 613-624

✦ Subjects

Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs