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

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
2022/3, Trimester 2, FACE-TO-FACE, Edinburgh Napier University
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 worksheets 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 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.

There is one two-hour lecture each week, covering both the theory and practical material. Lectures are also supported by directed study, with the course texts 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.
These case studies are implemented during practical sessions and further augmented by the students to further their understanding of the principles being taught. Seminar sessions are aimed at covering LO3, LO4 and LO5 by allowing the you to discuss real world examples and compare them to you 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 you are progressing with their 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 your 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 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

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