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

Module Code SET08108
Module Title Object Oriented Software Development
Examples of Equivalent Learning 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
2023/4, Trimester 2, FACE-TO-FACE, Edinburgh Napier University
VIEW FULL DETAILS
Occurrence: 001
Primary mode of delivery: FACE-TO-FACE
Location of delivery: MERCHISTON
Partner: Edinburgh Napier University
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)
Face To Face Lecture 24
Face To Face Practical classes and workshops 24
Independent Learning Guided independent study 152
Total Study Hours200
Expected Total Study Hours for Module200


Assessment
Type of Assessment Weighting % LOs covered Week due Length in Hours/Words
Practical Skills Assessment 075.00 1, 2, 4, 5 14/15 HOURS= 40.00, WORDS= 000.00
Class Test 025.00 3, 4 13 HOURS= 01.00, WORDS= 000.00
Component 1 subtotal: 75
Component 2 subtotal: 25
Module subtotal: 100

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