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

Nội dung tài liệu: Luận án Methods for modeling and verifying event-driven systems

1. 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
2. VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING AND TECHNOLOGY Lê Hồng Anh METHODS FOR MODELING AN D 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
3. ĐẠ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
4. 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
5. VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING AND TECHNOLOGY Lê Hồng Anh METHODS FOR MODELING AN D 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
6. ĐẠ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
7. VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING AND TECHNOLOGY Lê Hồng Anh METHODS FOR MODELING AN D 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
8. ĐẠ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
9. 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.
10. 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