Mô tả các phương pháp hình thức cho đặc tả phần mềm, các khái niệm về thành phần phần mềm, đặc tả thành phần phần mềm, máy hữu hạn trạng thái, hệ chuyển trạng thái được gán nhãn và ôtômát hữu hạn trạng thái. Nghiên cứu phương pháp xây dựng tự động mô hình mô tả chính xác hành vi của một thành phần phần mềm. Qua đó đề xuất giải pháp cho việc xây dựng mô hình thành phần phần mềm. Đưa ra kết quả thực nghiệm: công cụ sinh mô hình của một thành phần phần mềm và.