Tiến Sĩ Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện

Abstract

Modeling and verification plays an important role in software engineering because it improves the reliability of software systems. Software development technologies introduce a variety of methods or architectural styles. Each system based on a different architecture is often proposed with different suitable approaches to verify its correctness. Among these architectures, the field of event-driven architecture is broad in both academia and industry resulting the amount of work on modeling and verification of event-driven systems.
The goals of this thesis are to propose effective methods for modeling and verification of event-driven systems that react to emitted events using Event-Condition-Action (ECA) rules and Fuzzy If-Then rules. This thesis considers the particular characteristics and the special issues attaching with specific types such as database and context-aware systems, then uses Event-B and its supporting tools to analyze these systems.

First, we introduce a new method to formalize a database system including triggers by proposing a set of rules for translating database elements to Event-B constructs. After the modeling, we can formally check the data constraint preservation property and detect the infinite loops of the system.

Second, the thesis proposes a method which employs Event-B refinement for incrementally modeling and verifying context-aware systems which also use ECA rules to adapt the context situation changes. Context constraints preservation are proved automatically with the Rodin tool.

Third, the thesis works further on modeling event-driven systems whose behavior is specified by Fuzzy If-Then rules. We present a refinement-based approach to modeling both discrete and timed systems described with imprecise requirements.

Finally, we make use of Event-B refinement and existing reasoning methods to verify both safety and eventuality properties of imprecise systems requirements.

Contents
Declaration of Authorship i
Abstract ii
Acknowledgements iii
Table of Contents iv
List of Abbreviations viii
List of Tables ix
List of Figures x
1 Introduction 1
1.1 Motivation 1
1.2 Objectives 6
1.3 Literature review 7
1.4 Contributions 10
1.5 Thesis structure . 11
2 Backgrounds 13
2.1 Temporal logic . 13
2.2 Classical set theory . 15
2.3 Fuzzy sets and Fuzzy If-Then rules 17
2.3.1 Fuzzy sets 17
2.3.2 Fuzzy If-Then rules . 18
2.4 Formal methods . 19
2.4.1 VDM . 21
2.4.2 Z . 23
2.4.3 B method 24
2.5 Event-B . 27
2.5.1 An overview . 27
iv
Contents v
2.5.2 Event-B context . 28
2.5.3 Event-B Machine 29
2.5.4 Event-B mathematical language 31
2.5.5 Refinement . 32
2.5.6 Proof obligations 33
2.6 Rodin tool 36
2.7 Event-driven systems 37
2.7.1 Event-driven architecture 37
2.7.2 Database systems and database triggers . 38
2.7.3 Context-aware systems . 40
2.8 Chapter conclusions . 42
3 Modeling and verifying database trigger systems 44
3.1 Introduction . 44
3.2 Related work 47
3.3 Modeling and verifying database triggers system . 48
3.3.1 Modeling database systems 49
3.3.2 Formalizing triggers . 50
3.3.3 Verifying system properties 53
3.4 A case study: Human resources management application 54
3.4.1 Scenario description 54
3.4.2 Scenario modeling 55
3.4.3 Checking properties . 57
3.5 Support tool: Trigger2B 59
3.5.1 Architecture . 59
3.5.2 Implementation . 60
3.6 Chapter conclusions . 62
4 Modeling and verifying context-aware systems 64
4.1 Introduction . 64
4.2 Related work 66
4.3 Formalizing context awareness . 67
4.3.1 Set representation of context awareness 68
4.3.2 Modeling context-aware system 69
4.3.3 Incremental modeling using refinement 71
4.4 A case study: Adaptive Cruise Control system 72
4.4.1 Initial description 73
4.4.2 Modeling ACC system . 73
4.4.3 Refinement: Adding weather and road sensors 75
4.4.4 Verifying the system’s properties . 78
4.5 Chapter conclusions . 78
5 Modeling and verifying imprecise system requirements 81
5.1 Introduction . 81
5.2 Related work 83
Contents vi
5.3 Modeling fuzzy requirements 85
5.3.1 Representation of fuzzy terms in classical sets 85
5.3.2 Modeling discrete states 87
5.3.3 Modeling continuous behavior . 88
5.4 Verifying safety and eventuality properties 91
5.4.1 Convergence in Event-B 91
5.4.2 Safety and eventuality analysis in Event-B 92
5.4.3 Verifying safety properties . 93
5.4.4 Verifying eventuality properties 94
5.5 A case study: Container Crane Control 98
5.5.1 Scenario description 98
5.5.2 Modeling the Crane Container Control system 100
5.5.2.1 Modeling discrete behavior . 100
5.5.2.2 First Refinement: Modeling continuous behavior . 102
5.5.2.3 Second Refinement: Modeling eventuality property 104
5.5.3 Checking properties . 106
5.6 Chapter conclusions . 108
6 Conclusions 109
6.1 Achievements 109
6.2 Limitations . 113
6.3 Future work . 114
List of Publications 116
Bibliography 117
A Event-B specification of Trigger example 128
A.1 Context specification of Trigger example . 128
A.2 Machine specification of Trigger example . 129
B Event-B specification of the ACC system 132
B.1 Context specification of ACC system . 132
B.2 Machine specification of ACC system . 133
B.3 Extended context 134
B.4 Refined machine . 134
C Event-B specifications and proof obligations of Crane Controller Example
136
C.1 Context specification of Crane Controller system . 136
C.2 Extended context 137
C.3 Machine specification of Crane Controller system 138
C.4 Refined machine . 140
C.5 Proof obligations for checking the safety property 143
Contents vii
C.6 Proof obligations for checking convergence properties 144