Trong dự án này, chúng tôi sẽ nghiên cứu các phương pháp hình thức dựa trên thành phần để giải quyết vấn đề sự phức tạp của phần mềm trong thiết kế cũng như trong cài đặt. Ý tưởng là một hệ thống quy mô lớn, phức tạp có thể được xây dựng từ các thành phần cơ bản, đơn giản. Phương pháp này rất linh hoạt trong việc tái sử dụng các thành phần cũng như trong việc sửa đổi, mở rộng của hệ thống._x000d_ Phương pháp kiểm tra hình thức mô hình được sử dụng để kiểm tra và bảo đảm tính chính xác của hệ thống. Chúng tôi đề xuất một phương pháp kiểm tra tĩnh sử dụng các kỹ thuật phân tích hiệu quả về cấu trúc và tương tác giữa các thành phần. Phương pháp này cũng có thể được tích hợp ngay trong giai đoạn xây dựng phần mềm để phát hiện lỗi sớm nhất có thể. Tuy nhiên, kiểm tra tĩnh không phải hiệu quả với tất cả các loại thuộc tính. Nhiều thuộc tính chỉ có thể kiểm tra hiệu quả trong quá trình hoạt động. Kiểm tra trong khi vận hành là một kỹ thuật hiệu quả để đảm bảo việc một hệ thống đáp ứng một hành vi mong muốn trong quá trình hoạt động. Để thực hiện việc kiểm tra đầy đủ, trong trường hợp gặp lỗi, chúng tôi đề xuất một phương pháp định vị lỗi để giúp các nhà phát triển có thể xác định dễ dàng và nhanh chóng vị trí xảy ra lỗi._x000d_ Kết quả dự kiến: _x000d_ - Các phương pháp và công cụ: môi trường đồng nhất cho BIP and Alloy, kiểm tra và định vị lỗi._x000d_ - Công trình công bố: 2 tạp chí khoa học quốc tế ISI; 5 hội nghị khoa học/tạp chí (quốc tế, quốc gia)_x000d_ - Đào tạo: 3 thạc sĩ, 7 kỹ sư