Mô tả
Giới thiệu các phương pháp hình thức trong kỹ thuật phần mềm với nội dung về logic mệnh đề và logic bậc nhất (cú pháp, ngữ nghĩa, lý thuyết chứng minh), ngôn ngữ đặc tả hình thức, phân tích có hạn và xác thực, công cụ đặc tả hình thức, và kiểm tra mô hình với máy trạng thái hữu hạn, logic theo thời gian, và công cụ kiểm tra mô hình.
Tiền đề
- Điều kiện tiên quyết: COMP 1805, SYSC 3120, và SYSC 4001.
Điều kiện và thủ tục
- Điều kiện tiên quyết: COMP 1805, SYSC 3120, và SYSC 4001.
- Ba giờ giảng mỗi tuần.
Văn bản tham chiếu bằng ngôn ngữ gốc
Introduction to formal methods in software engineering with coverage of propositional and first-order logic (syntax, semantics, proof theory), formal specification languages, bounded analysis and validation, formal specification tools, and model checking with finite-state machines, temporal logic, and model checking tools.
- Prerequisite(s): COMP 1805 , SYSC 3120 , and SYSC 4001 .
- Lectures three hours a week.
Nguồn và tham khảo
Ngày và nguồn được giữ lại để giúp bạn kiểm tra thông tin. Các bản dịch được cung cấp để dễ đọc; nguồn chính thức là tham chiếu cho các điều kiện và yêu cầu.
Nguồn tham khảo : https://calendar.carleton.ca/undergrad/courses/SYSC/