Formal Methods in Software Engineering

Academic year: 2007-2008

Local KeyFORMP Hemis KeyU11497 Base Key3652
Credit Points15 LecturerDr Matthew Poole CoordinatorDr Alexander Gegov
Delivery ModeCampus - Semesterised Release StatusA Materials 
Normal LevelM Notional Study Hours150 Standard Hours36
Scheduled ActivitiesLecture = 20, Tutorial = 10, Assessment = 6. Min Student Numbers20 Max Student Numbers0
Prereq NamedNone Postreq NamedNone Coreq NamedNone
Excluded CombinationsNone DependanciesNone Prereq StatementStudents should be confident in the use of mathematical concepts of sets, functions and predicate logic and an understanding of the basic principles and techniques in formal methods.
Ass Weight Exam60 Ass Weight Con  Ass Weight Other40

Abstract

This extends students' knowledge of formal specification within the context of complex systems. The advantages and disadvantages of different types of formal specification will be considered and one specification language will be studied in depth.

Aims

To enable students to evaluate and use formal specifications in developing complex systems. 

Learning Outcomes

On successful completion of this unit, students should be able, at threshold level, to:

Summarise the characteristics of a formal specification. 
Validate formal specifications written in a formal language. 
Prepare specifications in a formal language. 
Recommend and justify an appropriate type of formal specification for a given application. 
Evaluate software tools to analyse and develop formal specifications. 

Learning and Teaching Strategy

New material will be introduced in lectures with practical sessions used to consolidate understanding. Case studies will be used to illustrate concepts as they are introduced.

Overall Assessment Strategy

Overall Assessment Strategy – to ensure students can demonstrate both a theoretical understanding of the learning outcomes and the ability to apply and evaluate their knowledge. In order to achieve a pass mark in this unit, a student must achieve a minimum mark of 30% in each assessment component as well as an overall aggregate mark of 40%. (APC approved exemption from University Examination and Assessment Regulations.)

Assessment Schedule and Strategy

Examination  60  Open book, 2 hours duration, individual, tutor-marked covering learning outcomes 1-4 
Supervised Work Session  40  A tutor-marked day long session with students both working in groups and individually on a practical piece of work involving elements of learning outcomes 2, 3 and 5. 

Named awards using this unit

Pathway Name Unit Level Semester Status Pathway Status
MSc Software Engineering   
MSc Electronic Commerce with Marketing   

Syllabus Outline

The topics covered in the unit will include:

Comparison of different types of formal specification (e.g. algebraic, model based, process algebra). 
Detailed study of a model based formal specification language (e.g. B, Z, VD, PD or OCL). 
Tool support for formal specification. 
Synthesis of a formal specification with a graphic notation eg UML 
Formal Specification for requirements engineering. 

Work Plan

Nil

Indicative Reading

  Warner, J. and Kleppe, A., The Object Constraint Language: Precise Modeling with UML, Addison Wesley, 1999, 0201379406, Y 
  Jackson, M., Software Requirement and Specifications, Addison Wesley, 1995, 0201877120, Y 
  Currie, E., The Essence of Z, Upper Saddle River NJ, Prentice Hall, 1999, 013749839X, Y 
  Nissanke, N, Formal Specification: Techniques and Applications, Springer-Verlag, 1999, 1852330023, Y 
  Fitzgerald, J. and Larson, P., Modelling Systems Practical Tools and Techniques in Software Development, CUP, 1998, 0521623480, Y 

Practicals

Nil

Resources

Nil

Level 3 Key Skills Opportunities

Key Skills CO  Key Skills NO  Key Skills IT 
Key Skills PS  Key Skills ILP  Key Skills WO 

Administrative details

Owning DepartmentSchool of Computing Programme AreaComputing and Multimedia Owning InstitutionUniversity of Portsmouth
Assessment BoardComputer Science and Software Engineering Responsible FHQATechnology Subject GroupSoftware Engineering
External ExaminerDr Neil Willis Programme CoordDr Christopher Lester University Cost Centre 
Effective Session2006/07 Withdrawn Date  Suspend Date 
Review Date  Major Release Date2003-06-03 00:00:00 Minor Release Date 

Notes

Robert Topp will be assisted in delivery by Alex Gegov. Access to a tool to support the chosen specification language will be needed. The unit will begin with a review of the relevant mathematical concepts aimed at students who have been out of higher education for some years. If required additional mathematical support will be available to students via the Maths Café and Maths Centre. Subject to timetabling constraints this unit may be offered as an option throughout the Postgraduate Programme.

History

History Version History Date Change Style History Detail
1.0  2003-06-03 00:00:00  New unit. (Mo Adda/RJS) 
1.1  2003-09-15 00:00:00  Overall assessment strategy detailing exemption added. Pathways revised. (Rod Jeffcote/RJS) Ext Examiner entered as Hope. (Annette Wilson/RJS) 
1.1  2003-11-17 00:00:00  Hemis code added (NS) 
1.2  2004-02-09 00:00:00  Unit code changed from SE.FORMP to FORMP (Annette Wilson/KW). 
1.3  2005-12-15 00:00:00  Minor Amendment to Lecturer and Semester ( Alex Gegov/KB) 
1.4  2006-02-22 00:00:00  Removed DM, ISD & ISY pathway (MS/JH) 
1.5  2006-11-17 00:00:00  External Examiner updated (C Faircloth) 
Last updated at 1323 on 22/1/2007. © University of Portsmouth. E&OE