Core Module Information
Module title: Formal Approaches to Software Engineering

SCQF level: 10:
SCQF credit value: 20.00
ECTS credit value: 10

Module code: SET10112
Module leader: Peter Chapman
School School of Computing, Engineering and the Built Environment
Subject area group: Computer Science
Prerequisites

Requisites: Pre-requisite: An understanding of software development/software engineering to an advanced level as indicated by study at SCQF level 8

Description of module content:

This module aims to provide you with a strong formal methods underpinning for usage in real world software development problems. By integrating an industrial tool and technique into your existing software development skills, you will learn to reason about and develop your software in a more correct and reliable manner. The module itself forms around a technology which can be integrated into a software development process. Ada-SPARK is a formal language of component / object based systems, with an underpinning in formal mathematical models. Various levels of formality are provided within Ada-SPARK, from absence of runtime errors (AoRTE), through to full proof of functional specifications. Students will experience the differing amount of effort to achieve each level.The module covers two main streams. A mathematical underpinning for software development is provided via material presented on logic, set theory, and proof. Ada-SPARK, used in safety-critical industrial applications, is introduced, and forms the basis of the coding instruction.The module covers the following topics:• Formal methods and their usage in industry and software development in general• Ada as a programming language• Ada-SPARK to support reliable and correct software development• Logic, set theory, and proof theory• Structuring complex software• Proving program correctness via preconditions and proof obligations

Learning Outcomes for module:

Upon completion of this module you will be able to

LO1: Produce a design and specification for an application using a formal approach.

LO2: Plan and develop an application which conforms to the obligations defined in a formal design and specification.

LO3: Critically assess the advantages and disadvantages that formal methods bring to the software development process.

LO4: Evaluate formal methods in comparison with other software development processes and development methodologies.

LO5: Integrate a formal approach into an existing software development process.

Full Details of Teaching and Assessment
2024/5, Trimester 2, In Person,
VIEW FULL DETAILS
Occurrence: 001
Primary mode of delivery: In Person
Location of delivery: MERCHISTON
Partner:
Member of staff responsible for delivering module: Peter Chapman
Module Organiser:


Student Activity (Notional Equivalent Study Hours (NESH))
Mode of activityLearning & Teaching ActivityNESH (Study Hours)NESH Description
Face To Face Lecture 20 The lectures consist of a series of worked examples, based on pre-recorded material. They are interactive, are recorded, and the notes and video made available after the event.
Face To Face Practical classes and workshops 20 The practicals will give you hand-on experience with the tools and techniques you have studied in the lectures. Feedback will be given on your studies during these sessions.
Online Guided independent study 160 You will be given readings and other materials to ensure you have command and mastery of the module content.
Total Study Hours200
Expected Total Study Hours for Module200


Assessment
Type of Assessment Weighting % LOs covered Week due Length in Hours/Words Description
Class Test 25 2~3 Week 13 HOURS= 1 Hour In the class test, you will perform the foundational calculations which underpin formal methods. These include writing and evaluating formal proofs, and calculations arising from the logics presented in the module. You will thus be able to assess the advantages (correctness) and disadvantages (difficulty) of the formal software development process.The weekly exercise sheets will help prepare you for the test, and you can receive formative feedback on your work throughout the semester.
Practical Skills Assessment 75 1~2~4~5 Exam Period HOURS= 40 Hours In this coursework, you will design and develop a software system for a safety-critical system. You will show it is correct, alongside developing the documentation that is expected of such systems.During the development of your system, you will have the opportunity to receive feedback on your work.
Component 1 subtotal: 75
Component 2 subtotal: 25
Module subtotal: 100

Indicative References and Reading List - URL:
Contact your module leader