Core Module Information
Module title: Formal Approaches to Software Engineering

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

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

Object-oriented software development to an equivalent of 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. You 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
2022/3, 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:


Learning, Teaching and Assessment (LTA) Approach:
This module adopts a blended approach within formative laboratory-based practicals, discussion tutorials and seminars, and lectures. Practical lab based instruction is supported with VLE resources aimed at reinforcing some of the principles discussed in lectures and tutorials, with further directed study also provided. Practical labs are supported by a workbook where you complete work assignments and also describe the methodologies that you have undertaken. Practical work will also focus on specific examples that build up to a coherent body of knowledge within the workbook. Material on VLE will be used to augment this workbook and provide a bridge between the practical and lecture material. The practical work, workbook and online material is aimed at supporting LO1, LO2 and LO5 by providing the necessary skills to develop software in a formal manner, including the underlying formal principles, numerous case examples and the necessary hands-on development practice.
The module delivery is four one-day sessions per semester, where you will get a mixture of both lectures and practical classes.. Lectures are designed to cover the theory as well as a high level view of the material that is presented in the practical sessions. Lectures are also supported by directed study, with the course text utilised extensively as further reading each week. The lectures are aligned with LO1, LO3, LO4 and LO5. The lectures provide the discussion on the ideas that are applied in the practical sessions. The lectures will also highlight the advantages and disadvantages of formal approaches, compare said approaches against other software development methods, and integrate a formal method into existing development processes.
Seminar sessions are designed to encourage student discussion by examining individual case studies and designing solutions for these case studies. These case studies are implemented during practical sessions and further augmented by you to further your understanding of the principles being taught. Seminar sessions are aimed at covering LO3, LO4 and LO5 by allowing you to discuss real world examples and compare them to your own understanding with the methods used in formal models.

Formative Assessment:
To support formative feedback, the Software Engineering subject group utilise a lab based teaching approach across their provision. During these lab sessions, staff will discuss and evaluate your progress and provide feedback on how well they are progressing with your work. All modules in the subject group also require you to demonstrate their coursework on submission to provide further formative feedback on how the work could be improved.

Summative Assessment:
The laboratory work and seminars will be a series of formative exercises which shall lead up to a summative assessment within the coursework. You will be supported during this process by feedback at various stages of the design process. This covers LO1, LO2, LO4 and LO5 by allowing you to apply the skills taught during the practical sessions in a piece of practical work, and discuss how well the formal method can be used in such problems.
Lectures are designed to overview the material as well as encourage discussion on the practicalities of formal methods within software engineering. These lectures, supported by the directed study material, are designed to provide you with the ability to approach the summative test. Therefore the test is aligned with LO3 and LO4 by allowing you to discuss their understanding of the advantages and disadvantages of formal software engineering and their application against other development processes.




Student Activity (Notional Equivalent Study Hours (NESH))
Mode of activityLearning & Teaching ActivityNESH (Study Hours)
Face To Face Practical classes and workshops 24
Independent Learning Guided independent study 152
Face To Face Lecture 24
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 75 1, 2, 4, 5 14/15 HOURS= 40.00
Class Test 25 3, 4 13 HOURS= 01.00
Component 1 subtotal: 75
Component 2 subtotal: 25
Module subtotal: 100

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