Nghiên cứu mô hình kiến trúc phần mềm hiện đại dựa trên thành phần và các công nghệ nền tảng như CORBA, Java Beans, .NET và web-service để đưa ra các phương pháp đặc tả, kiểm chứng nhằm mục đích tăng chất lượng của các hệ thống xây dựng dựa trên các công nghệ này. Nghiên cứu các phương pháp mô hình hóa các hệ thống phần mềm phức tạp và các mô hình tích hợp hệ thống. Nghiên cứu các phương pháp và ngôn ngữ đặc tả giao diện tương tác thành phần phần mềm, đặc biệt là đặc tả dựa trên phương pháp hình thức. Nghiên cứu các phương pháp kiểm chứng phần mềm: kiểm chứng thành phần phần mềm ở các mức mô hình, mã nguồn và mã thực thi, kiểm chứng sự tương thích về giao diện của các thành phần phần mềm, kiểm chứng sự tương thích về môi trường và ràng buộc về tài nguyên, kiểm chứng các ràng buộc thời gian thực. Phát triển cức công cụ trợ giúp như: bộ phân tích cú pháp và sinh mã; bộ phân tích mã đối tượng và xây dựng đồ thị luồng điều khiển, bộ chứng minh tự động. Nghiên cứu ứng dụng các công cụ mô hình hóa và kiểm chứng như: SPIN, SMV, B4 free, Java Path Finder, ... Kết quả đạt được: Phương pháp sinh giả định tối thiểu kiểm chứng phần mềm dựa trên thành phần. Phương pháp kiểm chứng sự tuân thủ giữa thực thi so với đặc tả thiết kế. Phương pháp kiểm chứng hình thức cho các hệ thống tương tranh. Phương pháp sinh bộ kiểm thức thích hợp cho việc chuyển đổi số thực dấu phẩy động sang số thực dấu phẩy tĩnh