INFS 3008 Formal Software Engineering

Credit Points 10

Legacy Code 300404

Coordinator Yan Zhang Opens in new window

Description This subject is concerned with the design, development and maintenance of computer software systems. The subject focuses on current formal specification and system verification technologies and methodologies. Foundations of model checking such as Linear Temporal Logic and Computation Tree Logic, as well as a particular practical model checker SPIN will be thoroughly studied in this subject. The SPIN model checker with programming language PROMELA will be used for all software development and verification practices throughout this subject. The subject plays an important part in preparing students for career paths as software engineers and IT developers.

School Computer, Data & Math Sciences

Discipline Programming

Student Contribution Band HECS Band 2 10cp

Check your fees via the Fees page.

Level Undergraduate Level 3 subject

Pre-requisite(s) MATH 1006 AND
COMP 2009

Learning Outcomes

On successful completion of this subject, students should be able to:

1. Describe the general concepts and principles of formal methods for software development and verification
2. Model concurrent systems using the concepts and principles of transition systems and program graphs.
3. Adapt Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) to specify the required properties for software systems.
4. Formulate PROMELA programs and apply SPIN model checker to specify and verify the correctness of various software systems and programs.
5. Evaluate different formal methods in relation to the performance of formal specification and verification tasks for various practical software systems.
6. Develop a functional verification prototype system for an actual software project, using advanced SPIN model checker and PROMELA programming methodologies.

Subject Content

Concept and Development of Formal Methods and System Verifications.
Modeling Concurrent Systems.
Linear Time Properties.
Linear Temporal Logic (LTL).
Computation Tree Logic (CTL).
SPIN Model Checker.
PROMELA Programming Language.

Assessment

The following table summarises the standard assessment tasks for this subject. Please note this is a guide only. Assessment tasks are regularly updated, where there is a difference your Learning Guide takes precedence.