Formal Methods and Software Engineering: 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, October 21-25, 2002, ... (Lecture Notes in Computer Science, 2495)

✍ Scribed by Chris George (editor), Huaikou Miao (editor)

• Publisher: Springer
• Year: 2002
• Tongue: English
• Leaves: 639
• 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

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