INFS 3008 Formal Software Engineering

This is an archived copy of the 2021-2022 catalog. To access the most recent version of the catalog, please visit https://hbook.westernsydney.edu.au.

Credit Points 10

Legacy Code 300404

Coordinator Yan Zhang Opens in new window

Description This unit is concerned with the design, development and maintenance of computer software systems. The unit focuses on current formal specification and system verification technologies and methodologies. Foundations of model checking such as LTL and CTL, as well as a particular practical model checker SPIN will be thoroughly studied in this unit. The SPIN model checker with programming language PROMELA will be used for all software development and verification practices throughout this unit.

School Computer, Data & Math Sciences

Discipline Information Systems

Student Contribution Band HECS Band 2 10cp

Check your HECS Band contribution amount 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 formal notions of transition systems and program graphs.
  3. Apply Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) to specify the required properties.
  4. Perform model checking using SPIN model checker.
  5. Formulate PROMELA programs and using SPIN to specify and check the correctness of given software systems and programs.
  6. Apply the advanced verification tools to undertake essential formal specification and verification tasks.

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.

Item Length Percent Threshold Individual/Group Task
Practical To take place during practicals 60 N Individual
Quiz 1 1.5 hours 20 Y Individual
Quiz 2 1.5 hours 20 Y Individual

Teaching Periods

Spring

Penrith (Kingswood)

Day

Subject Contact Yan Zhang Opens in new window

View timetable Opens in new window

Parramatta - Victoria Rd

Day

Subject Contact Yan Zhang Opens in new window

View timetable Opens in new window

Structures that include subject