›
›

Luận án Methods for modeling and verifying event-driven systems

Download
VIETNAM NATIONAL UNIVERSITY, HANOI  
UNIVERSITY OF ENGINEERING AND TECHNOLOGY  
LÊ HỒNG ANH  
METHODS FOR MODELING AND  
VERIFYING EVENT-DRIVEN SYSTEMS  
DOTORAL THESIS IN INFORMATION TECHNOLOGY  
Hà Nội – 2015  
VIETNAM NATIONAL UNIVERSITY, HANOI  
UNIVERSITY OF ENGINEERING AND TECHNOLOGY  
Lê Hồng Anh  
METHODS FOR MODELING AND VERIFYING EVENT-DRIVEN  
SYSTEMS  
Major: Software Engineering  
Mã số: 62.48.01.03  
DOCTORAL THESIS IN INFORMATION TECHNOLOGY  
SUPERVISORS:  
1. Assoc. Prof. Dr. Trương Ninh Thuận  
2. Assoc. Prof. Dr. Phạm Bảo Sơn  
Hà Nội – 2015  
ĐẠI HỌC QUỐC GIA HÀ NỘI  
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ  
Lê Hồng Anh  
PHƯƠNG PHÁP MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC HỆ  
THỐNG HƯỚNG SỰ KIỆN  
Chuyên ngành: Kỹ thuật phần mềm  
Mã số: 62.48.01.03  
LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN  
NGƯỜI HƯỚNG DẪN KHOA HỌC:  
1. PGS. TS. Trương Ninh Thuận  
2. PGS. TS. Phạm Bảo Sơn  
Hà Nội – 2015  
Declaration of Authorship  
I declare that this thesis titled, ‘Methods for modeling and verifying event-driven systems’  
and the work presented in it are my own. I confirm that:  
ꢀ
I have acknowledged all main sources of help. Where I have quoted from the work of  
others, the source is always given. With the exception of such quotations, this thesis is  
entirely my own work.  
ꢀ
ꢀ
Where the thesis is based on work done by myself jointly with others, I have made clear  
exactly what was done by others and what I have contributed myself.  
This work was done wholly while in studying for a PhD degree  
Signed:  
Date:  
i
VIETNAM NATIONAL UNIVERSITY, HANOI  
UNIVERSITY OF ENGINEERING AND TECHNOLOGY  
Lê Hồng Anh  
METHODS FOR MODELING AND VERIFYING EVENT-DRIVEN  
SYSTEMS  
Major: Software Engineering  
Mã số: 62.48.01.03  
DOCTORAL THESIS IN INFORMATION TECHNOLOGY  
SUPERVISORS:  
1. Assoc. Prof. Dr. Trương Ninh Thuận  
2. Assoc. Prof. Dr. Phạm Bảo Sơn  
Hà Nội – 2015  
ĐẠI HỌC QUỐC GIA HÀ NỘI  
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ  
Lê Hồng Anh  
PHƯƠNG PHÁP MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC HỆ  
THỐNG HƯỚNG SỰ KIỆN  
Chuyên ngành: Kỹ thuật phần mềm  
Mã số: 62.48.01.03  
LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN  
NGƯỜI HƯỚNG DẪN KHOA HỌC:  
1. PGS. TS. Trương Ninh Thuận  
2. PGS. TS. Phạm Bảo Sơn  
Hà Nội – 2015  
VIETNAM NATIONAL UNIVERSITY, HANOI  
UNIVERSITY OF ENGINEERING AND TECHNOLOGY  
Lê Hồng Anh  
METHODS FOR MODELING AND VERIFYING EVENT-DRIVEN  
SYSTEMS  
Major: Software Engineering  
Mã số: 62.48.01.03  
DOCTORAL THESIS IN INFORMATION TECHNOLOGY  
SUPERVISORS:  
1. Assoc. Prof. Dr. Trương Ninh Thuận  
2. Assoc. Prof. Dr. Phạm Bảo Sơn  
Hà Nội – 2015  
ĐẠI HỌC QUỐC GIA HÀ NỘI  
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ  
Lê Hồng Anh  
PHƯƠNG PHÁP MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC HỆ  
THỐNG HƯỚNG SỰ KIỆN  
Chuyên ngành: Kỹ thuật phần mềm  
Mã số: 62.48.01.03  
LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN  
NGƯỜI HƯỚNG DẪN KHOA HỌC:  
1. PGS. TS. Trương Ninh Thuận  
2. PGS. TS. Phạm Bảo Sơn  
Hà Nội – 2015  
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 pro-  
posed 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 propos-  
ing 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.  
Acknowledgements  
First of all, I would like to express my sincere gratitude to my first supervisor Assoc. Prof.  
Dr. Truong Ninh Thuan and my second supervisor Assoc. Prof. Pham Bao Son for their  
support and guidance. They not only teach me how to conduct research work but also show  
me how to find passion on science.  
Besides my supervisors, I also would like to thank Assoc. Prof. Dr. Nguyen Viet Ha and  
lecturers at Software Engineering department for their valuable comments about my research  
work in each seminar.  
I would like to thank Professor Shin Nakajima for his support and guidance during my intern-  
ship research at National Institute of Informatics, Japan.  
My sincere thanks also goes to Hanoi University of Mining and Geology and my colleges there  
for their support during my PhD study.  
Last but not least, I would like to thank my family: my parents, my wife, my children for  
their unconditional support in every aspect. I would not complete the thesis without their  
encouragement.  
. . .  
iii  
Contents  
Declaration of Authorship  
i
Abstract  
ii  
Acknowledgements  
iii  
Table of Contents  
List of Abbreviations  
List of Tables  
iv  
viii  
ix  
List of Figures  
x
1 Introduction  
1
1
6
7
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .  
1.2 Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .  
1.3 Literature review . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .  
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  
Bibliography  
116  
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 Ex-  
ample  
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  
List of Abbreviations  
DDL  
DML  
PO  
Data Dafinition Language  
Data Manipulation Language  
Proof Obligation  
LTL  
Linear Temporal Logic  
Software Cost Reduction  
Event Condition Action  
Vienna Development Method  
SCR  
ECA  
VDM  
VDM-SL Vienna Development Method - Specification Language  
FM  
Formal Method  
PTL  
CTL  
SCR  
AMN  
Propositional Temporal Logic  
Computational Temporal Logic  
Software Cost Reduction  
Abstract Machine Notation  
viii  
List of Tables  
2.1 Truth tables for propositional operators . . . . . . . . . . . . . . . . . . 14  
2.2 Meaning of temporal operators . . . . . . . . . . . . . . . . . . . . . . 15  
2.3 Truth table of implication operator . . . . . . . . . . . . . . . . . . . . 19  
2.4 Comparison of B, Z and VDM [1] . . . . . . . . . . . . . . . . . . . . . 27  
2.5 Relations and functions in Event-B . . . . . . . . . . . . . . . . . . . . 32  
2.6 INV proof obligation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  
2.7 VAR PO with numeric variant . . . . . . . . . . . . . . . . . . . . . . . 35  
2.8 VAR PO with finite set variant . . . . . . . . . . . . . . . . . . . . . . 35  
3.1 Translation rules between database and Event-B . . . . . . . . . . . . . 50  
3.2 Formalizing a trigger . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  
3.3 Encoding trigger actions . . . . . . . . . . . . . . . . . . . . . . . . . . 53  
3.4 Table EMPLOYEES and BONUS . . . . . . . . . . . . . . . . . . . . . 55  
3.5 INV PO of event trigger1. . . . . . . . . . . . . . . . . . . . . . . . . . 58  
3.6 Infinite loop proof obligation of event trigger1 . . . . . . . . . . . . . . 59  
4.1 Modeling a context rule by an Event-B Event . . . . . . . . . . . . . . 70  
4.2 Transformation between context-aware systems and Event-B . . . . . . 70  
4.3 Proof of context constraint preservation . . . . . . . . . . . . . . . . . . 78  
5.1 INV PO of event evt4 . . . . . . . . . . . . . . . . . . . . . . . . . . . 106  
5.2 Deadlock free PO of machine Crane M 1 . . . . . . . . . . . . . . . . . 107  
5.3 VAR PO of event evt4 . . . . . . . . . . . . . . . . . . . . . . . . . . . 108  
C.1 INV PO of event evt1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 143  
C.2 INV PO of event evt2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 143  
C.3 INV PO of event evt3 . . . . . . . . . . . . . . . . . . . . . . . . . . . 143  
C.4 INV PO of event evt5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 144  
C.5 VAR PO of event evt1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 144  
C.6 NAT PO of event evt1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 144  
C.7 VAR PO of event evt2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 144  
C.8 NAT PO of event evt2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 145  
C.9 VAR PO of event evt3 . . . . . . . . . . . . . . . . . . . . . . . . . . . 145  
C.10 NAT PO of event evt3 . . . . . . . . . . . . . . . . . . . . . . . . . . . 145  
C.11 VAR PO of event evt5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 145  
C.12 NAT PO of event evt5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 145  
ix  
List of Figures  
1.1 Types of event-driven systems . . . . . . . . . . . . . . . . . . . . . . .  
3
1.2 Thesis structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12  
2.1 Basic structure of an Event B model . . . . . . . . . . . . . . . . . . . 28  
2.2 An Event-B context example . . . . . . . . . . . . . . . . . . . . . . . 29  
2.3 Forms of Event-B Events . . . . . . . . . . . . . . . . . . . . . . . . . . 30  
2.4 Event-B refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  
2.5 Event refinement in Event-B . . . . . . . . . . . . . . . . . . . . . . . . 33  
2.6 A convergent event . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  
2.7 The Rodin tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  
2.8 A layered conceptual framework for context-aware systems [2] . . . . . 41  
3.1 Partial Event-B specification for a database system . . . . . . . . . . . 51  
3.2 A part of Event-B Context . . . . . . . . . . . . . . . . . . . . . . . . 56  
3.3 A part of Event-B machine . . . . . . . . . . . . . . . . . . . . . . . . 57  
3.4 Encoding trigger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  
3.5 Architecture of Trigger2B tool . . . . . . . . . . . . . . . . . . . . . . 60  
3.6 A partial parsed tree syntax of a general trigger . . . . . . . . . . . . . 61  
3.7 The modeling result of the scenario generated by Trigger2B . . . . . . 62  
4.1 A simple context-aware system . . . . . . . . . . . . . . . . . . . . . . 68  
4.2 Incremental modeling using refinement . . . . . . . . . . . . . . . . . . 71  
4.3 Abstract Event-B model for ACC system . . . . . . . . . . . . . . . . 75  
4.4 Events with strengthened guards . . . . . . . . . . . . . . . . . . . . . 76  
4.5 Refined Event-B model for ACC system . . . . . . . . . . . . . . . . . 77  
4.6 Checking properties in Rodin . . . . . . . . . . . . . . . . . . . . . . . 79  
5.1 A part of Event-B specification for discrete transitions modeling . . . . 89  
5.2 A part of Event-B specification for continuous transitions modeling . . 90  
5.3 A part of Event-B specification for eventuality property modeling . . . 96  
5.4 Container Crane Control system . . . . . . . . . . . . . . . . . . . . . . 98  
5.5 Safety properties are ensured in the Rodin tool automatically . . . . . . 107  
x
Chapter 1  
Introduction  
1.1 Motivation  
Nowadays, software systems become more complex and can be used to  
integrate with other systems. Software engineers need to understand as  
much as possible what they are developing. Modeling is one of effective  
ways to handle the complexity of software development that allows to  
design and assess the system requirements. Modeling not only represents  
the content visually but also provides textual content. There are sev-  
eral types of modeling language including graphical, textual, algebraic  
languages.  
In software systems, errors may cause many damages for not only eco-  
nomics but also human beings, especially those applications in embed-  
ded systems, transportation control and health service equipment, etc.  
The error usually occurs when the system execution cannot satisfy the  
characteristics and constraints of the software system specification. The  
specification is the description of the required functionality and behavior  
of the software. Therefore, ensuring the correctness of software systems  
1
Chapter 1. Introduction  
2
has always been a challenge of software development process and relia-  
bility plays an important role deciding the success of a software project.  
Testing techniques are used in normal development in order to check  
whether the software execution satisfies users requirements. However,  
testing is an incomplete validation because it can only identifies errors  
but can not ensure that the software execution is correct in all cases.  
Software verification is one of powerful methods to find or mathemati-  
cally prove the absent of software errors. Several techniques and methods  
have been proposed for software verification such as model-checking [3],  
theorem-proving [4] and program analysis [5]. Among these techniques,  
theorem proving has distinct advantages such as superior size of the sys-  
tem and its ability to reason inductively. Though, theorem proving often  
generates a lot of proofs which are complex to understand. Verification  
techniques mainly can be classified into two kinds: model-level and im-  
plementation level. Early verification of model specifications helps to  
reduce the cost of software construction. For this reason, modeling and  
verification of software systems are an emerging research topic in around  
the world. Many approaches and techniques of modeling and verification  
have been proposed so far. Each of them usually focuses on a typical  
kind of software architecture or design styles.  
In a traditional system, one component provides a collection of proce-  
dures and functions via its interfaces. Components then interact with  
each other by explicitly invoking those routines. Event-driven architec-  
ture is one of the most popular architectures in software project develop-  
ment providing implicit invocation instead of invoking routines directly.  
Each component of an event-driven system can produce events, the sys-  
tem then invoke all procedures which are registered with these events. An  
Chapter 1. Introduction  
3
event-driven system consists of three essential parts: monitoring compo-  
nent, transmission component and responsive one. Since such systems  
work by raising and responding to events, it looses coupling between  
software components and improves the interactive capabilities with its  
environment. The event-driven architectural style is becoming an essen-  
tial part of large-scale distributed systems design and many applications.  
It is a promising architecture to develop and model loosely coupled sys-  
tems and its advantages have been recognized in both academia and  
industry.  
There are many types of event-driven systems including many editors  
where user interface events signify editing commands, rule-based pro-  
duction systems where a condition becoming true causes an action to  
be triggered and active objects where changing a value of an object’s  
attribute triggers some actions (e.g. database trigger systems) [6]. Fig-  
ure 1.1 shows the hierarchy of listed event-driven systems. In this thesis,  
we consider two applications of active objects and rule-based production  
systems: database systems with triggers and context-aware systems.  
Event−driven systems  
Graphic user interfaces Rule−based production systems Active objects  
...  
Context−aware systems  
Database trigger systems  
Figure 1.1: Types of event-driven systems  
In event-driven systems, Event-Condition-Action (ECA) rules are pro-  
posed as a declarative approach to specify relations when certain events  
occur at predefined conditions. An ECA rule has the form: On Event  
Tải về để xem bản đầy đủ
pdf 174 trang yennguyen 22340 Free
Download
Bạn đang xem 20 trang mẫu của tài liệu "Luận án Methods for modeling and verifying event-driven systems", để tải tài liệu gốc về máy hãy click vào nút Download ở trên

File đính kèm:

  • pdfluan_an_methods_for_modeling_and_verifying_event_driven_syst.pdf