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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Acknowledgements First of all, I would like to express my sincere gratitude to my first supervisor Assoc. Truong Ninh Thuan and my second supervisor Assoc. 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. 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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.2 Classical set theory .3 Fuzzy sets and Fuzzy If-Then rules .2 Fuzzy If-Then rules . 27 iv LUAN VAN CHAT LUONG download : add luanvanchat@agmail.4 Event-B mathematical language .7 Event-driven systems .1 Event-driven architecture .2 Database systems and database triggers .3 Context-aware systems . 42 3 Modeling and verifying database trigger systems 44 3.3 Modeling and verifying database triggers system .1 Modeling database systems .3 Verifying system properties .4 A case study: Human resources management application .5 Support tool: Trigger2B . 62 4 Modeling and verifying context-aware systems 64 4.3 Formalizing context awareness .1 Set representation of context awareness .2 Modeling context-aware system .3 Incremental modeling using refinement .4 A case study: Adaptive Cruise Control system .2 Modeling ACC system .3 Refinement: Adding weather and road sensors .4 Verifying the system’s properties . 78 5 Modeling and verifying imprecise system requirements 81 5. 83 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Contents vi 5.3 Modeling fuzzy requirements .1 Representation of fuzzy terms in classical sets .2 Modeling discrete states .3 Modeling continuous behavior .4 Verifying safety and eventuality properties .1 Convergence in Event-B .2 Safety and eventuality analysis in Event-B .3 Verifying safety properties .4 Verifying eventuality properties .5 A case study: Container Crane Control .2 Modeling the Crane Container Control system .1 Modeling discrete behavior .2 First Refinement: Modeling continuous behavior .3 Second Refinement: Modeling eventuality property . 114 List of Publications 116 Bibliography 117 A Event-B specification of Trigger example 128 A.1 Context specification of Trigger example .2 Machine specification of Trigger example . 129 B Event-B specification of the ACC system 132 B.1 Context specification of ACC system .2 Machine specification of ACC system . 134 C Event-B specifications and proof obligations of Crane Controller Ex- ample 136 C.1 Context specification of Crane Controller system .3 Machine specification of Crane Controller system .5 Proof obligations for checking the safety property . 143 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Contents vii C.6 Proof obligations for checking convergence properties . 144 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com List of Abbreviations DDL Data Dafinition Language DML Data Manipulation Language PO Proof Obligation LTL Linear Temporal Logic SCR Software Cost Reduction ECA Event Condition Action VDM Vienna Development Method VDM-SL Vienna Development Method - Specification Language FM Formal Method PTL Propositional Temporal Logic CTL Computational Temporal Logic SCR Software Cost Reduction AMN Abstract Machine Notation viii LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com List of Tables 2.1 Truth tables for propositional operators .2 Meaning of temporal operators .3 Truth table of implication operator .4 Comparison of B, Z and VDM [1] .5 Relations and functions in Event-B .6 INV proof obligation .7 VAR PO with numeric variant .8 VAR PO with finite set variant .1 Translation rules between database and Event-B .3 Encoding trigger actions .4 Table EMPLOYEES and BONUS .5 INV PO of event trigger 1.6 Infinite loop proof obligation of event trigger 1 .1 Modeling a context rule by an Event-B Event .2 Transformation between context-aware systems and Event-B .3 Proof of context constraint preservation .1 INV PO of event evt4 .2 Deadlock free PO of machine Crane M 1 .3 VAR PO of event evt4 .1 INV PO of event evt1 .2 INV PO of event evt2 .3 INV PO of event evt3 .4 INV PO of event evt5 .5 VAR PO of event evt1 .6 NAT PO of event evt1 .7 VAR PO of event evt2 .8 NAT PO of event evt2 .9 VAR PO of event evt3 .10 NAT PO of event evt3 .11 VAR PO of event evt5 .12 NAT PO of event evt5 . 145 ix LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com List of Figures 1.1 Types of event-driven systems .1 Basic structure of an Event B model .2 An Event-B context example .3 Forms of Event-B Events .5 Event refinement in Event-B .7 The Rodin tool .8 A layered conceptual framework for context-aware systems [2] .1 Partial Event-B specification for a database system .2 A part of Event-B Context .3 A part of Event-B machine .5 Architecture of Trigger2B tool .6 A partial parsed tree syntax of a general trigger .7 The modeling result of the scenario generated by Trigger2B .1 A simple context-aware system .2 Incremental modeling using refinement .3 Abstract Event-B model for ACC system .4 Events with strengthened guards .5 Refined Event-B model for ACC system .6 Checking properties in Rodin .1 A part of Event-B specification for discrete transitions modeling .2 A part of Event-B specification for continuous transitions modeling .3 A part of Event-B specification for eventuality property modeling .4 Container Crane Control system .5 Safety properties are ensured in the Rodin tool automatically . 107 x LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. 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. database trigger systems) [6].1 shows the hierarchy of listed event-driven systems.
Luận văn VNU UET: Phương pháp mô hình hóa và kiểm chứng hệ thống hướng sự kiện
Luận văn thạc sĩ VNU UET trình bày các phương pháp mô hình hóa và kiểm chứng hệ thống hướng sự kiện, mang lại giải pháp hiệu quả cho nghiên cứu.
Trường đại học
Hanoi University of Mining and GeologyChuyên ngành
Software EngineeringNgười đăng
Ẩn danhThể loại
thesis2023
155
1
0
Phí lưu trữ
45 PointMục lục chi tiết
Tóm tắt
I. Phương pháp mô hình hóa hệ thống hướng sự kiện hiệu quả
Mô hình hóa và kiểm chứng các hệ thống hướng sự kiện là một lĩnh vực quan trọng trong kỹ thuật phần mềm. Các phương pháp này giúp cải thiện độ tin cậy của hệ thống phần mềm, đặc biệt trong các ứng dụng phức tạp. Luận văn này sẽ trình bày các phương pháp mô hình hóa và kiểm chứng hiệu quả cho các hệ thống này, sử dụng các quy tắc ECA và các quy tắc Fuzzy If-Then.
1.1. Tổng quan về hệ thống hướng sự kiện
Hệ thống hướng sự kiện là một kiến trúc phần mềm cho phép các thành phần tương tác thông qua các sự kiện. Kiến trúc này giúp giảm sự phụ thuộc giữa các thành phần và cải thiện khả năng tương tác với môi trường.
1.2. Tầm quan trọng của mô hình hóa trong kỹ thuật phần mềm
Mô hình hóa giúp các kỹ sư phần mềm hiểu rõ hơn về yêu cầu và chức năng của hệ thống. Nó không chỉ giúp thiết kế mà còn đánh giá các yêu cầu của hệ thống một cách hiệu quả.
II. Thách thức trong việc kiểm chứng hệ thống hướng sự kiện
Việc kiểm chứng các hệ thống hướng sự kiện gặp nhiều thách thức do tính phức tạp và sự không chắc chắn trong yêu cầu. Các phương pháp hiện tại thường không đủ để xử lý các yêu cầu mơ hồ hoặc không chính xác.
2.1. Các vấn đề trong kiểm chứng hệ thống
Nhiều phương pháp kiểm chứng hiện tại chỉ tập trung vào các mô tả chính xác của chức năng và hành vi của hệ thống, dẫn đến việc thiếu sót trong việc xử lý các yêu cầu không chính xác.
2.2. Tác động của yêu cầu không chính xác đến hệ thống
Yêu cầu không chính xác có thể dẫn đến các lỗi nghiêm trọng trong hệ thống, ảnh hưởng đến hiệu suất và độ tin cậy của phần mềm.
III. Các phương pháp mô hình hóa hệ thống hướng sự kiện
Luận văn này đề xuất các phương pháp mô hình hóa mới cho các hệ thống hướng sự kiện, bao gồm việc sử dụng các quy tắc ECA và các quy tắc Fuzzy If-Then để mô hình hóa hành vi của hệ thống.
3.1. Mô hình hóa hệ thống cơ sở dữ liệu với quy tắc ECA
Phương pháp này sử dụng các quy tắc ECA để mô hình hóa các hệ thống cơ sở dữ liệu, cho phép kiểm chứng các thuộc tính của hệ thống một cách chính xác.
3.2. Mô hình hóa hệ thống nhận thức ngữ cảnh
Hệ thống nhận thức ngữ cảnh sử dụng các quy tắc ECA để thích ứng với các thay đổi trong ngữ cảnh, giúp cải thiện khả năng tương tác của hệ thống.
IV. Kết quả nghiên cứu và ứng dụng thực tiễn
Nghiên cứu đã chỉ ra rằng các phương pháp mô hình hóa và kiểm chứng mới có thể cải thiện đáng kể độ tin cậy của các hệ thống hướng sự kiện. Các ứng dụng thực tiễn cho thấy tính khả thi và hiệu quả của các phương pháp này.
4.1. Ứng dụng trong hệ thống cơ sở dữ liệu
Các phương pháp mô hình hóa đã được áp dụng thành công trong các hệ thống cơ sở dữ liệu, giúp phát hiện và sửa chữa các lỗi trong quá trình phát triển.
4.2. Ứng dụng trong hệ thống nhận thức ngữ cảnh
Nghiên cứu cho thấy rằng các phương pháp này có thể được áp dụng để phát triển các hệ thống nhận thức ngữ cảnh hiệu quả hơn, cải thiện khả năng thích ứng với môi trường.
V. Kết luận và triển vọng tương lai của nghiên cứu
Luận văn đã đề xuất các phương pháp mới cho mô hình hóa và kiểm chứng các hệ thống hướng sự kiện. Tương lai của nghiên cứu này hứa hẹn sẽ mở ra nhiều cơ hội mới trong lĩnh vực kỹ thuật phần mềm.
5.1. Tương lai của mô hình hóa hệ thống hướng sự kiện
Các phương pháp mới có thể được phát triển để xử lý các yêu cầu không chính xác, mở rộng khả năng của các hệ thống hướng sự kiện.
5.2. Hướng nghiên cứu tiếp theo
Nghiên cứu có thể tiếp tục mở rộng sang các lĩnh vực khác như hệ thống nhúng và các ứng dụng trong ngành công nghiệp, nhằm cải thiện độ tin cậy và hiệu suất của phần mềm.
22/07/2025
TÀI LIỆU LIÊN QUAN
Bạn đang xem trước tài liệu:
Luận văn thạc sĩ vnu uet methods for modeling and verifying event driven systems phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện
THÔNG TIN CHI TIẾT
Người hướng dẫn: Assoc. Truong Ninh Thuan
Trường học: Hanoi University of Mining and Geology
Chuyên ngành: Software Engineering
Đề tài: Methods for Modeling and Verifying Event-Driven Systems
Loại tài liệu: thesis
Năm xuất bản: 2023
Địa điểm: Hanoi
Trích đoạn nội dung tài liệu
Nội dung được bảo vệ bản quyền — Tải xuống đầy đủ