KF6009 - Model Based Design and Verification

APPLY NOW Book an Open Day Add to My Courses Register your interest / Course PDF

What will I learn on this module?

On this module you will learn the theory and practice of modelling, specification and analysis for the development of computer software. You will be introduced to a variety of formal methods, such as state transition systems, timed and probabilistic automata, and temporal logic You are encouraged to construct, analyse and refine your own system models. In addition, you will gain experience with state-of-the-art software engineering tools for design and analysis.

In particular the module will cover topics such as:
• Modelling - variety of formal methods, e.g.:, , state transition systems, timed and probabilistic automata; use of abstraction; modelling of functional, temporal and security aspects of system behaviour
• Specification – propositional, predicate and temporal logic; safety and liveness properties: deadlock freedom, fairness, bounded response, security
• Analysis - principles of model-checking, simulation, and static analysis for reasoning about system behaviour
• Tools - use of tools, e.g.: Uppaal, Spin, PRISM and evaluation of their outputs.

How will I learn on this module?

Lectures are the main vehicle by which you will be introduced to fundamental concepts and principles and for providing context and motivation. You will be expected to prepare for lecture topics and deepen your understanding of course material by studying course texts and technical literature. Seminars and practical sessions support the lecture programme by providing you with opportunities to identify defend and apply appropriate methods and tools for specification and design. Software tools are available outside formal contact time to enable you to explore aspects of the subject independently.

How will I be supported academically on this module?

In the seminars and practical sessions you will have the opportunity to discuss your solutions to the exercises with other students and staff, gaining formative feedback to aid your knowledge and understanding. In addition, the eLP (electronic learning portal module) blackboard is used to provide extensive support materials and to make model exercise solutions available to help you assess your understanding.

What will I be expected to read on this module?

All modules at Northumbria include a range of reading materials that students are expected to engage with. The reading list for this module can be found at: http://readinglists.northumbria.ac.uk
(Reading List service online guide for academic staff this containing contact details for the Reading List team – http://library.northumbria.ac.uk/readinglists)

What will I be expected to achieve?

Knowledge & Understanding:
1. Discuss the theoretical principles of various formal methods for the specification and design of computer software, and the algorithms and data structures used in their supporting tools.

Intellectual / Professional skills & abilities:
2. Construct and evaluate formal models of a variety of computer systems.
3. Compose formal specifications of system properties and analyse system models with respect to them.
4. Identify, apply and evaluate appropriate software tools to support the construction and analysis of formal system models and properties.

Personal Values Attributes (Global / Cultural awareness, Ethics, Curiosity) (PVA):
5. Evaluate the advantages and disadvantages of the application of various formal methods in the development of computer software, and justify their use where appropriate, having regard to professional, ethical, technical and security issues.

How will I be assessed?

Formative assessment takes the form of weekly exercises which are intended to reinforce your understanding of the concepts and techniques of software specification and design. The exercises are collaborative, requiring you to discuss and justify your decisions, methods and solutions both with other students and with academic staff. You will have opportunities to discuss your exercise solutions with academic staff in the weekly practical sessions.

Summative assessment comprises a single coursework assignment. You will be given an informal system specification and will be required to develop formal models and specifications of a design for the system. You will be required to use appropriate techniques and tools to analyse and evaluate your designs and will be required to show understanding of the principles underlying the approaches that you adopt. You will be required to report on aspects of your models, specification and analysis results.

Written feedback is provided on the summative assessment. The assignment assesses all of the MLOs.

Pre-requisite(s)

None

Co-requisite(s)

None

Module abstract

On this module you will learn the theory and practice of modelling, specification and analysis for the development of computer software. You will be introduced to a variety of formal methods, such as state transition systems, timed and probabilistic automata, and temporal logic You are encouraged to construct, analyse and refine your own system models. In addition, you will gain experience with state-of-the-art software engineering tools for design and analysis.

Course info

UCAS Code G404

Credits 20

Level of Study Undergraduate

Mode of Study 3 years full-time or 4 years with a placement (sandwich)/study abroad

Department Computer and Information Sciences

Location Pandon Building, Newcastle City Campus

City Newcastle

Start September 2019

Current, Relevant and Inspiring

We continuously review and improve course content in consultation with our students and employers. To make sure we can inform you of any changes to your course register for updates on the course page.

Your Learning Experience find out about our distinctive approach at 
www.northumbria.ac.uk/exp

Terms and Conditions - northumbria.ac.uk/terms
Fees and Funding - northumbria.ac.uk/fees
Admissions Policy - northumbria.ac.uk/adpolicy