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

Formal Methods and Software Engineering
Preface
Table of Contents
SFI: A Refinement Based Layered Software Architecture
	References
Developing Quality Software Systems Using the SOFL Formal Engineering Method
	1 Introduction
	2 Formal Engineering Methods
	3 The SOFL Specification Language
	4 The SOFL Method
		4.1 The Process Model
		4.2 Example
	5 Rigorous Review
		5.1 Steps for Rigorous Reviews
		5.2 Properties of Specifications
	6 Specification Testing
	7 Conclusions
	References
Maintaining Referential Integrity on the Web
	High Value Applications
	Web Application Management
	Referential Integrity
	Next Step: Web Services
Formal Methods in Enterprise Computing
	Extended Abstract
Unifying Theories of Parallel Programming
	1 Introduction
	2 Unifying Theories of Programming
	3 Action Systems
	4 Labelled Action Systems
	5 Syntax and Semantics
	6 Concurrent Hoare Logic
	7 Example
	8 Conclusion
	References
ABC/ADL: An ADL Supporting Component Composition
	1 Introduction
	2 Features of ABC/ADL
		2.1 Component Model
		2.2 Design Principles
		2.3 Type and Instance
		2.4 Architecture, Composite Component and Component Evolution
		2.5 Pluggable Style
		2.6 Complex Connector
		2.7 Aspect
	3 Constructs in ABC/ADL
		3.1 Component and Connector
		3.2 Architecture
		3.3 Style
		3.4 Semantic Description
	4 Tool Support
	5 Related Work
		5.1 Other ADLs
		5.2 Component Based Software Development (CBSD)
	6 Conclusion
	Acknowledgements
	References
The Description of CORBA Objects Based on Petri Nets
	1 Introduction
	2 CORBA
		2.1 The CORBA Object Model
		2.2 CORBA Object Services
	2.3 CORBA Specification
	3 CORBA Objects Formalism
		3.1 Petri Nets Basics
		3.2 CORBA Object Description Based Petri Nets Rules
	4 Conclusions
	Acknowledgements
	References
Toward a Formal Model of Software Components
	1 Introduction
	2 Introduction to JavaBeans
	3 The JavaBean Component Model
		3.1 Top-Level Model
		3.2 Constrained Properties
	4 Specification of a Bean
	5 Related Work
	6 Conclusions
	References
A Specification-Based Software Construction Framework for Reuse
	1 Introduction
	2 Construction Framework
		2.1 Reuse Oriented Framework
		2.2 Design Space and High-Level Component Construction
	3 Component Matching
		3.1 Matching Function
		3.2 Matching Definition
	4 Components Composition
	5 Conclusion
	References
Specifying a Component Model for Building Dynamically Reconfigurable Distributed Systems
	1 Introduction
	2 Dynamically Reconfigurable Component-Based Distributed Systems
	3 Component Model for Dynamic Reconfiguration
		3.1 Component Structure
		3.2 Static Dependencies Among Components
		3.3 Dynamic Dependencies among Components
		3.4 Inter-component Interaction
		3.5 State Diagram of Components
	4 Related Work
		4.1 Current Component Models
		4.2 Dynamic Reconfiguration of Distributed Systems
	5 Conclusions and Future Work
	Acknowledgments
	References
Three-Tiered Specification of Micro-architectures
	1 Micro-architectures
	2 Specification in Three Tiers
		2.1 Lowest Tier: Structure
		2.2 Middle Tier: Roles
		2.3 Highest Tier: Interaction
	3 Conclusion
Modeling the Architecture for Component-Based E-commerce System
	1 Introduction
	2 The Reference Architecture of E-commerce System
		2.1 Related Works
		2.2 Classification of Component
		2.3 Reference Architecture of E-commerce System
	3 Modeling Component-Based E-commerce System
		3.1 Component Dependency Graph
		3.2 Layering of a Component-Based System
		3.3 Finding Key Components
		3.4 The Reuse of Component
		3.5 Connectivity of Component
	4 Conclusion and Future Works
	References
Component Specification and Wrapper/Glue Code Generation with Two-Level Grammar Using Domain Specific Knowledge
	1 Introduction
	2 Specification with Two-Level Grammar
	3 An Example
		3.1 User Level Component Model Specification
		3.2 System Level Component Assembly Specification
	4 Conclusion
	References
Abstract Specification in Object-Z and CSP
	1 Introduction
	2 Illustrative Example
	3 Abstraction
	4 Refinement
		4.1 Introducing an Explicit Communication Mechanism
	5 Conclusion
	Acknowledgement
	References
Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS
	1 Introduction
	2 An Overview of Configuration Machines
	3 An Overview of SAL
	4 Systematic Translation of Specifications into SAL
		4.1 Abstraction of Configuration Machines
		4.2 Abstraction of SAL Modules
		4.3 Translation Rules
		4.4 Embedding of the Data Part into PVS: Z2PVS
		4.5 Translation of Machines Composition
	5 An Experiment Report
	6 Related Works and Concluding Remarks
	References
Concept Use or Concept Refinement: An Important Distinction in Building Generic Specifications
	1 Introduction
	2 Concepts and Concept Descriptions
	3 Tecton Definitions
	4 Inheritance from Previous Concept Descriptions
	5 Concept Instances
		5.1 The Simple Case
		5.2 The General Case
		5.3 Legality Requirements for Replacements
		5.4 Tecton Abbreviations
	6 Concluding Remarks
	References
An Overview of Mobile Object-Z
	1 Introduction
	2 Syntax
	3 Operational Semantics
	4 Examples
		4.1 Forwarding
		4.2 Tracking
	5 Language Features
	6 Related Work and Conclusion
	Acknowledgements
	References
Z Approach to Semantic Web
	1 Introduction
	2 Semantic Web Overview
	3 The Talks Discovery System
		3.1 System Scenario
		3.2 Formal Models of the Talk Discovery System
	4 Extracting DAML Ontology from the Z Model
		4.1 Given Type Transformation
		4.2 Z Axiomatic (Function and Relation) Definition Transformation
		4.3 Z Axiomatic (Subset and Constant) Definition Transformation
		4.4 Z Schema Transformation
	5 Improve the Ontology Quality through Z Tools
	6 Conclusion
	Acknowledgements
	References
Hardware/Software Partitioning in Verilog
	1 Introduction
	2 Verilog and Its Algebraic Laws
	3 Partitioning Strategy
	4 Hardware/Software Partitioning Framework
	5 Hardware/Software Partitioning
		5.1 Syntax-Based Splitting Rules for Kernel Specification
		5.2 Deriving Hw/Sw Partition for an Environment-Driven System
	6 Conclusion and Future Work
	References
A Formal Methodology to Specify E-commerce Systems
	1 Introduction
	2 Model Checking of E-commerce Systems
		2.1 Business Rules
		2.2 Symbolic Model Checking
	3 The Formal Specification Methodology
		3.1 Properties of an E-commerce System
		3.2 Conceptual Level
		3.3 Application Level
		3.4 Functional Level
		3.5 Architectural Level
	4 Case Study: An E-commerce Virtual Store
		4.1 Conceptual Level
		4.2 Application Level
		4.3 Functional Level
		4.4 Architectural Level
	5 Related Work
	6 Conclusions and Future Work
	References
Model-Based Specification Animation Using Testgraphs
	1 Introduction
	2 Related Work
		2.1 Animation
		2.2 Testing Using Graphs and Finite State Machines
	3 Background
		3.1 Example – IntSet
		3.2 Possum
	4 Animation Using Testgraphs
		4.1 Deriving a Testgraph
		4.2 Traversing the Testgraph
		4.3 Checking States and Operations
	5 Tool Support
		5.1 Constructing a Testgraph
		5.2 Generating Paths
		5.3 Traversing the Testgraph
		5.4 Report Generation
		5.5 Advanced Features
		5.6 Experience
	6 Conclusions and Future Work
	References
An Abstract Model for Scheduling Real-Time Programs
	1 Introduction
	2 The Source Language
	3 The Target Language
	4 An Abstract Model for Scheduling
	5 Cyclic Scheduling
	6 Fixed Priority Scheduling with Pre-emption
		6.1 Verifying Computational Behaviour
		6.2 Verifying Timing Constraints
	7 Conclusion
	Acknowledgments
	References
A Specification and Validation Technique Based on STATEMATE and FNLOG
	1 Introduction
	2 General View of the Proposed Specification and Validation Method
	3 Conclusion
	References
Formal Representation and Analysis of Batch Stock Trading Systems by Logical Petri Net Workflows
	1 Introduction
	2 Logical Petri Net Workflows
	3 LPNW of the Batch Stock Trading System
	4 Properties Analysis Based on LPNW
	Acknowledgements
	References
A Calculus for Mobile Network Systems
	1 Introduction
	2 Mobility in Mobile Network Systems
	3 The Entity Calculus
	4 Conclusion
	Acknowledgments
	References
Modelling Real-Time Systems with Continuous-Time Temporal Logic
	1 Introduction
	2 LTLC: Syntax and Semantics
	3 Representing Real-Time Systems with LTLC
	4 Conclusion
	References
On Concept-Based Definition of Domain-Specific Languages
	1 Introduction
	2 Element Concept
		2.1 Dynamic Semantics
		2.2 Static Semantics
	3 Complement Concept
	4 Defining DSLs Using DD
	5 Related and Future Work
	References
Formal Specification of Evolutionary Software Agents
	1 Introduction
	2 Review of the Language and Methodology
		2.1 The Underlying Model
		2.2 The SLABS Language
		2.3 The Development Process
		2.4 Diagrammatic Representation of Agent Models
	3 Case Study: Amalthaea
		3.1 System's Architecture and Interactions between the Agents
		3.2 Scenario Analysis and Description of Behaviour
		3.3 Decomposition and Analysis of Internal Structure
	4 Conclusion
	References
Detecting Deadlock in Ada Rendezvous Flow Structure Based on Process Algebra
	1 Introduction
	2 Preliminaries
	3 ACP Description of Ada Rendezvous
	4 ACP Description of Ada Rendezvous Flow Structure
	5 Deadlock Detection in Ada Rendezvous Flow Structure
		5.1 Basic Definitions
		5.2 Detection of Complete Deadlock Cycles
		5.3 Detection of Partial Deadlock Cycles
	6 Case Study
	7 Conclusions
	References
Formal Analysis of Real-Time Systems with SAM
	1 Introduction
	2 Real-Time Modeling in SAM
		2.1 The SAM Specification Structure
		2.2 PrTNs and Behavior Modeling
		2.3 LTL and Property Specification
	3 Formal Analysis of SAM Models
		3.1 A Formal Analysis Method
		3.2 Clocked Transition Systems
		3.3 From PrTNs to CTSs
	4 An Example: Consistency of SMIL Documents
	5 Conclusion
	References
Tool Support for Visualizing CSP in UML
	1 Introduction
	2 CSP
	3 UML
		3.1 State Diagrams
		3.2 Class Diagram
	4 Our Approach
		4.1 Visualizing the Dynamic Behavior of CSP
		4.2 Visualizing the Static Structure of CSP
		4.3 Visualizing CSP Refinement Assertion
	5 Case Study: The Lift System
		5.1 Dynamic Behavior View
		5.2 Static Structure View
		5.3 Refinement View
		5.4 The Overview
	6 Conclusion
	References
Theorem Prover Support for Precondition and Correctness Calculation
	1 Introduction
	2 Related Work
	3 The Correctness/Precondition Calculator
		3.1 Language Embedding
		3.2 Basic Calculations
		3.3 Angelic Statements
		3.4 Loops
		3.5 Procedures and Adaptation
		3.6 Recursive Procedures
		3.7 Simplification
	4 Examples
		4.1 Angelic and Demonic Nondeterminism
		4.2 Nested and Recursive Procedures
		4.3 Arrays and Multiple Loops
	5 Conclusion
	References
XML-Based Static Type Checking and Dynamic Visualization for TCOZ
	1 Introduction
	2 Technical Background
		2.1 TCOZ
		2.2 XML and XMI
	3 Type Checker Design and Typing Rules
		3.1 High-Level Design
		3.2 Type Hierarchy and Rules
	4 TCOZto UML Statechart Projection
	5 Case Study: Light Control System
		5.1 Static Type Checking
		5.2 Dynamic UML Visualizing
	6 Conclusions
	Acknowledgements
	References
µ-Chart-Based Specification and Refinement
	1 Introduction
	2 Introduction to mu-Charts
	3 The CSP Model
		3.1 Chart Refinement in the CSP Model
		3.2 Practicalities
	4 The Z Model
		4.1 Chart Refinement in the Z Model
	5 Comparing Refinement Relations
	6 Conclusions
	References
Towards a Refinement Calculus for Concurrent Real-Time Programs
	1 Introduction
	2 Language and Meaning
		2.1 The Real-Time Specification Command
		2.2 Primitive Real-Time Commands
		2.3 Compound Real-Time Commands
	3 Communication via Message Passing
		3.1 Introduction of a New Channel
		3.2 Sending and Receiving Messages
	4 Refinement
	5 An Example
	6 Conclusion and Further Work
	Acknowledgements
	References
Refinement Algebra for Formal Bytecode Generation
	1 Introduction
	2 The ROOL Language and Its Laws
	3 Interpreter Structure
	4 Compiling with Theorems
		4.1 Simplification of Expressions
		4.2 Data Refinement
		4.3 Control Elimination
		4.4 Lemmas
		4.5 Proof Example
	5 Conclusions
	Acknowledgments
	References
Formal Modelling of Java GUI Event Handling
	1 Motivation
	2 Java GUI Event Handling Mechanism
	3 Operational Semantics for the Event Handling
	4 An Example
	5 Detecting Errors
	6 Related Work
	7 Conclusion and Final Remarks
	Acknowledgements
	References
A New Algorithm for Service Interaction Detection
	1 Introduction
	2 Basics
	3 Feature Interaction Detection Algorithm
		3.1 Acyclic Paths and Simple Loops Generation  in a Finite State Machine
		3.2 Scenarios Analysis
		3.3 Feature Interactions Detection Strategy
	4 Application to a Case Study
	5 Conclusion
	References
Specification of an Asynchronous On-chip Bus
	1 Introduction
	2 Action Systems
	3 Bus Components
	4 Specification
		4.1 Arbiter System
	5 Discussion
	6 Conclusions
	References
Analysis of a Security Protocol in µCRL
	1 Introduction
	2 The Needham-Schroeder Public-Key Protocol
	3 Analysis Process
		3.1 Algebraic Specification
		3.2 Stating the Correctness Properties
		3.3 Requirements of the Protocol
		3.4 Verification Results
	4 Conclusion and Future Work
	References
Developing a Spell-Checker for Tajik Using RAISE
	1 Introduction
	2 Tajik Language
	3 Language Modelling
	4 Developing the Spell Checker
	5 Conclusions
	References
M2Z: A Tool for Translating a Natural Language Software Specification into Z
	1 Introduction
	2 Translating Natural Language Text into Formal Notations
	3 Overview of M2Z
	4 Architecture of M2Z
	5 Conclusion
	References
Abstract Interpretation with a Theorem Prover
	1 Introduction
	2 Abstract Interpretation
	3 The HOL Theorem Prover
		3.1 Extending Theories in HOL
	4 A Logic for Analysis
		4.1 Equivalence Rules
		4.2 Abstraction Rules
		4.3 Example Analysis
	5 On Using HOL
		5.1 Transforms in HOL
		5.2 Proof in HOL
	6 Conclusion
	Acknowledgments
	References
Formal Reasoning about Hardware and Software Memory Models
	1 Introduction
	2 A Checker for Java Memory Model
	3 A Checker for SPARC Memory Models
	4 Relationship between Memory Models
		4.1 Avoiding Redundant Memory Barriers
		4.2 Reasoning about Unsynchronized Programs
	5 Discussions
	References
Slicing Hierarchical Automata for Model Checking UML Statecharts
	1 Introduction
	2 The Extended Hierarchical Automata
	3 Dependence Relations in EHA
	4 Slicing EHA for Model Checking UML Statecharts
		4.1 Compute EHA Slice
		4.2 Extract Slicing Criteria from LTL Formulas
	5 Conclusion
	References
Formal Verification of a SONET Telecom System Block
	1 Introduction
	2 Multiway Decision Graphs
	3 The RASE Telecom System Block
		3.1 MDG Modeling of the RASE Implementation
		3.2 MDG Modeling of the RASE Behavior
	4 Verification of the RASE TSB
		4.1 Model Checking of the RASE TSB
		4.2 Equivalence Checking of the RASE TSB
	5 Comparison with FormalCheck
	6 Conclusions
	Acknowledgments
	References
Enabling Hardware Verification through Design Changes
	1 Introduction
	2 The IEEE-754 Exponential Function
	3 Modeling and Verification Methodology
	4 Formal Specification of IEEE-754 Exponential Function
	5 Formal Verification of the Exponential Function
	6 Conclusions
	References
Specification-Based Test Generation for Security-Critical Systems Using Mutations
	1 Introduction
	2 Security Models in AUTOFOCUS
	3 Generating Test Sequences for Vulnerabilities
		3.1 Vulnerability Coverage Using Mutations
		3.2 Concretization of Abstract Tests
	4 Related Work
	5 Conclusion
	References
A Formal Definition of Function Points for Automated Measurement of B Specifications
	1 Introduction
	2 Overview of Functions Points
	3 Overview of the B Method
		3.1 Example of a B Specification
	4 Formal Definition Summary
	5 Classifying Components
	6 Weighing Components
	7 The UFP Counting Algorithm
	8 Case Study
	9 Conclusion
	References
Machine Code Type Safety
	1 Introduction
	2 Our Approach
	3 Conclusion
	References
On the Formalized Semantics of Static Modeling Elements in UML
	1 Introduction
	2 The Necessity of UML’s Formal Semantics
	3 Two Aspects of Phraseology Description
	4 Formal Semantics of Some Common Modeling Elements in UML
		4.1 Class and Object
		4.2 Generalization (for Class)
		4.3 Binary Association and Other Extend Association
		4.4 Aggregation
		4.5 Roles
		4.6 Powertype
		4.7 Template Class
		4.8 Interface
		4.9 Type
		4.10 Metaclass
	5 Conclusions and Expectation
	References
From a B Specification to UML StateChart Diagrams
	1 Introduction
	2 Overall View of B Method
	3 Statecharts Diagrams
		3.1 Introduction
		3.2 Presentation
		3.3 Notation
	4 Extraction of Statechart Diagrams
		4.1 Introduction
		4.2 Approach
		4.3 The Example of the Robot
		4.4 Extraction of Statechart Diagram from the Abstract System
		4.5 Extraction of Statechart Diagrams from a Refined Systems
	5 Conclusion and Further Works
	References
Formalizing UML Models with Object-Z
	1 Introduction
	2 Formalizing the UML Class Diagram
		2.1 Class
		2.2 Association
		2.3 Association Class
		2.4 Class Diagram
	3 Formalizing UML Sequence Diagram
		3.1 Message
		3.2 Sequence Diagram
	4 Formalizing UML Statechart Diagram
		4.1 State
		4.2 Transition
	5 OZRose – A Tool for Transforming UML Models into Object-Z
		5.1 The Framework of OZRose
		5.2 The Executing Process of OZRose
	6 Conclusion
	References
Using Transition Systems to Unify UML Models
	1 Introduction
	2 Conceptual Model
		2.1 Conceptual Class Diagram
		2.2 Semantics of Class Conceptual Diagrams
		2.3 Object Diagrams as System States
		2.4 State Assertions
		2.5 Conceptual Models
	3 Use-Case Model
		3.1 System Operations
		3.2 Actors Operations
		3.3 Constructing a System Specification
	4 Conclusion and Discussion
	References
A Formal Metamodeling Approach to a Transformation between the UML State Machine and Object-Z
	1 Introduction
	2 Background
		2.1 An Object-Z Model of the UML State Machine
		2.2 The Object-Z Metamodel Defining core Modeling Concepts
	3 A Formal Mapping between the UML State Machine and Object-Z
	4 Conclusions
	References
A UML Approach to the Design of Open Distributed Systems
	1 Introduction
	2 Interactive Multimedia Kiosk
	3 Open Distributed Processing
		3.1 ODP Computational Viewpoint of the IMK
	4 A UML Approach to Computational Viewpoint Modelling
		4.1 Computational Metamodel Diagram
	5 IMK as a Specific Domain of Application
		5.1 Computational Class Diagram for IMK Systems
		5.2 Computational Object Diagram of the Museum Information Kiosk
	6 Discussion
	7 Related Work and Conclusion
	References
A Semantic Model of Real-Time UML
	1 Introduction
	2 The UML Variant
	3 The Two-Dimensional Temporal Logic L_2
	4 Translating the UML Model into L_2
	5 Conclusions and Further Research
	References
Research on Ontology-Oriented Domain Analysis on MIS
	1 Introduction
	2 Related Work
	3 Ontology-Oriented Domain Analyzing on MIS
		3.1 Why do We Need Ontology?
		3.2 How to Introduce Ontology?
		3.3 Definition of Ontology and Its Inheritance Relationship
		3.4 The Improvement of ONONET
	4 Summary
	References
A Requirements Description Model Based on Conditional Directed Graphs
	1 Introduction
	2 Mathematical Descriptions of Business Flows
	3 Business-Oriented CDGRD Model
	4 An Application Instance
	5 Conclusions and Future Work
	References
Introducing Reference Semantics via Refinement
	1 Introduction
	2 Value Semantics
	3 Reference Semantics
	4 Refinement
		4.1 Phase 1: Replacing Object Values with References
		4.2 Phase 2: Adding References between Objects
		4.3 Phase 3: Replacing the System Class with an Object Class
	5 Conclusion
	Acknowledgements
	References
Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational Semantics
	1 Introduction
	2 Operational Semantics for Verilog
		2.1 Syntax for Verilog
		2.2 Transition Types
		2.3 Operational Semantics for Verilog
		2.4 Transition Condition and Phase Semantics
	3 Soundness
	4 Completeness
	5 Non-redundancy
		5.1 Logical Point of View for Operational Semantics
		5.2 Non-redundancy
	6 Conclusion
	References
	Appendix
Towards a Time Model for Circus
	1 Introduction
	2 CT*: Informal Description
	3 The Semantic Model
		3.1 Basic Actions
		3.2 Sequential Composition
		3.3 Guarded Action
		3.4 External Choice
		3.5 Recursion
		3.6 Timeout
	4 Linking Circus Models
	5 Example
	6 Conclusions
	References
Author Index