Formal Methods | BSE YR2 SEM 1

TEAM UNIVERSITY

FACULTY OF APPLIED SCIENCES
DEPARTMENT OF INFORMATION TECHNOLOGY

TEACHING PORTFOLIO

Lecturer: Muwanguzi Benard
Contact: +256708646603
Email: info@ictconnect.org | Email 2: muwanguzibenard2017@gmail.com

COURSE TITLE: BIT2205 – FORMAL METHODS

Course Description

This course introduces students to formal methods, which are mathematically based techniques for specifying, developing, and verifying software and hardware systems. The focus is on applying logic, algebraic specifications, and formal notations to ensure system correctness and reliability. Students gain exposure to predicate logic, formal specification methods, algebraic approaches, and supporting tools. The course emphasizes precision, rigor, and automation in software development, preparing learners to model complex systems, verify designs, and avoid ambiguities that often arise in informal approaches.

Course Objectives

The course aims to:
a) Introduce students to the foundational concepts of formal methods in software development.
b) Equip learners with knowledge of predicate logic and its application in reasoning about programs.
c) Provide skills in specifying systems using formal notations and algebraic approaches.
d) Expose students to tools and environments that support formal methods.
e) Enable learners to apply formal methods in modeling, specification, and verification of systems.

Learning Outcomes

By the end of the course, students should be able to:
a) Demonstrate understanding of predicate logic and apply it to reasoning about programs.
b) Specify system requirements using formal methods and notations.
c) Apply algebraic specification techniques in modeling systems.
d) Use tools and formal systems to analyze and verify correctness of specifications.
e) Explore extensions of formal methods such as statecharts and automatic program synthesis.

Detailed Course Description

• Unit 1: Predicate Logic (8 Hrs)
  Introduction to formal logic, syntax and semantics of predicate logic, propositions, quantifiers, inference rules, reasoning about programs.
• Unit 2: Specification (9 Hrs)
  Need for formal specification, specification languages, specification styles, requirements modeling, properties of good specifications (consistency, completeness, unambiguity).
• Unit 3: Tools and Systems of Formal Notations (10 Hrs)
  Overview of formal notation systems (e.g., Z, VDM, B-method), automated tools, theorem provers, model checkers, proof assistants, strengths and limitations of tools.
• Unit 4: Algebraic Specification (10 Hrs)
  Introduction to algebraic specification, data types and operations, equational reasoning, modular specifications, examples of algebraic specifications in practice.
• Unit 5: Other Topics (8 Hrs)
  Statecharts (visual formalism for complex systems), automatic program synthesis, application of formal methods in real-world systems (safety-critical, embedded systems).
• Unit 6: Tutorials (20 Hrs)
  Guided exercises, group work, case studies, hands-on practice with logic proofs, specification tasks, and use of selected tools.

Total Contact Hours: 45 Hrs

Mode of Delivery

• Lectures
• Tutorials
• Group discussions
• Case studies
• Demonstrations
• Practical tool usage

Mode of Assessment

• Continuous Assessment (30%) → Assignments, Tests, Presentations, Group Work
• Final Examination (70%)
• Total: 100%

References

1. Bowen, J. P. (2013). Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press.
2. Woodcock, J., & Davies, J. (2009). Using Z: Specification, Refinement, and Proof. Prentice Hall.
3. Gries, D., & Schneider, F. B. (2013). A Logical Approach to Discrete Math. Springer.
4. Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
5. Baier, C., & Katoen, J. P. (2008). Principles of Model Checking. MIT Press.

Grade Scale

• 80–100: A
• 75–79: B+
• 70–74: B
• 65–69: C+
• 60–64: C
• 55–59: D+
• 50–54: D
• 0–49: F