Module Catalogue 2014/15

CSC3323 : Software Verification Technologies

  • Offered for Year: 2014/15
  • Module Leader(s): Dr Leo Freitas
  • Owning School: Computing Science
Semesters
Semester 1 Credit Value: 10
ECTS Credits: 5.0
Pre Requisites
Code Title
CSC1022Programming II
CSC1025Mathematics for Computer Science
CSC2021Software Engineering
CSC2023Algorithm Design and Analysis
Pre Requisite Comment

N/A

Co Requisites
Co Requisite Comment

N/A

Aims

To train students with practical aspects of formal modelling and verification technology as parts of a well-founded set of tools and techniques within software engineering.

Outline Of Syllabus

1.       Background
1.1.       The nature of software (SW) verification; verification principles (correctness, concurrency, abstraction, refinement, design decisions, documented assumptions, model-based testing)
1.2.       Understanding expertise required and costs involved; identifying the right technique to the task at hand.
2.       Modelling and Specification
2.1.       From a requirements document and produce an initial abstract specification of the problem.
2.2.       Elicit properties of interest from these requirements as formal consistency conditions, and make a specification of them that is amenable to analysis and verification.
2.3.       Foundations of formal modelling: propositional and predicate logic, data types and invariants; state-based models; mathematical toolkits.
2.4.       Propose design decisions as improved specifications; designs must be amenable to proof and consistency checking of desired properties;
2.5.       Possibly propose code-level contracts from formal design.
3.       Verification & Validation
3.1.       Understand verification support systems able to discharge formal consistency conditions from modelling activities
3.2.       Understand what it means for one specification to be a design refinement of another by establishing a link from the requirements to code-contracts
3.3.       Study alternative (to formal) techniques aiming at understanding the costs and conditions under which to undertake a formal or rigorous development process.
3.4.       Understand the importance of automated proof support and proof engineering (i.e. the process of mechanising a complex model)
3.5.       Metrics for complexity, reliability, expertise, time costs

Learning Outcomes

Intended Knowledge Outcomes

On successful completion of the module, students will be able to describe:
1.       How abstraction can be used to capture informal requirements as a formal (mathematical) specification
2.       One or more formal specification languages (i.e. modelling language, proof support system language).
3.       What can be claimed about the system under design
4.       A working knowledge of proof support systems

Intended Skill Outcomes

To be able to make an informed choice from a range of formal software engineering tools and techniques, and to apply them to the development of realistic software and systems.

Graduate Skills Framework

Graduate Skills Framework Applicable: Yes
  • Cognitive/Intellectual Skills
    • Critical Thinking : Present
    • Numeracy : Present
    • Information Literacy
      • Synthesise And Present Materials : Present
  • Self Management
    • Self Awareness And Reflection : Present
    • Planning and Organisation
      • Goal Setting And Action Planning : Present
      • Decision Making : Present
    • Personal Enterprise
      • Independence : Present
      • Problem Solving : Assessed
      • Adaptability : Present
  • Interaction
    • Communication
      • Oral : Present
      • Interpersonal : Present
      • Written Other : Present
  • Application
    • Legal Awareness : Present

Teaching Methods

Teaching Activities
Category Activity Number Length Student Hours Comment
Guided Independent StudyAssessment preparation and completion280:3014:00Revision for end of Semester exam and exam duration
Guided Independent StudyAssessment preparation and completion241:0024:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesLecture241:0024:00Lectures
Scheduled Learning And Teaching ActivitiesLecture221:0022:00Background reading
Scheduled Learning And Teaching ActivitiesPractical81:008:00Practicals
Guided Independent StudyProject work81:008:00Coursework
Total100:00
Teaching Rationale And Relationship

Lectures provide the knowledge. Practicals to provide additional background.

Reading Lists

Assessment Methods

The format of resits will be determined by the Board of Examiners

Exams
Description Length Semester When Set Percentage Comment
Written Examination901A60Open book exam
Other Assessment
Description Semester When Set Percentage Comment
Prob solv exercises1M401 piece of coursework (15 hours)
Assessment Rationale And Relationship

The open book exam will assess knowledge. Coursework to reinforce some of the lecture material.

N.B. This module has both “Exam Assessment” and “Other Assessment” (e.g. coursework). If the total mark for either assessment falls below 35%, the maximum mark returned for the module will normally be 35%.

Timetable

Past Exam Papers

General Notes

Based on module CSC3304

Note: The Module Catalogue now reflects module information relating to academic year 14/15. Please contact your School Office if you require module information for a previous academic year.

Disclaimer: The University will use all reasonable endeavours to deliver modules in accordance with the descriptions set out in this catalogue. Every effort has been made to ensure the accuracy of the information, however, the University reserves the right to introduce changes to the information given including the addition, withdrawal or restructuring of modules if it considers such action to be necessary.