Doctoral thesis in Information technology: Methods for modeling and verifying event driven systems

The thesis directs at providing tools, which support for automatic trans-lation from an application of event-driven systems to a target Event-B model that makes less eort and reduces the diculties in modeling pro-cess. The output of these tools are expected to be able usable in the Event-B supporting tools such as Rodin.
Nội dung trích xuất từ tài liệu:
Doctoral thesis in Information technology: Methods for modeling and verifying event driven systems VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING AND TECHNOLOGY LÊ HỒNG ANH METHODS FOR MODELING ANDVERIFYING EVENT-DRIVEN SYSTEMS DOTORAL THESIS IN INFORMATION TECHNOLOGY Hà Nội – 2015 VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING AND TECHNOLOGY Lê Hồng AnhMETHODS 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 AnhPHƯƠ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 AuthorshipI 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 degreeSigned:Date: i VIETNAM NATIONAL UNIVERSITY, HANOI UNIVERSITY OF ENGINEERING AND TECHNOLOGY Lê Hồng AnhMETHODS 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 AnhPHƯƠ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 AnhMETHODS 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 AnhPHƯƠ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 – 2015AbstractModeling and verification plays an important role in software engineering because it improvesthe reliability of software systems. Software development technologies introduce a variety ofmethods 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 theamount of work on modeling and verification of event-driven systems.The goals of this thesis are to propose effective methods for modeling and verification ofevent-driven systems that react to emitted events usi ...