The descriptions are for modules currently being taught. They should be viewed as an example of the modules we provide. All modules are subject to change for later academic years.

Predictable Software Systems (PSS) 2010/1

Workload - Private Study - Assessment - Description - Learning Outcomes - Content - Teaching Materials - Recommended Books

Module Code 0660237
Lecturers vis
Taken By LSCITS 1, LSCITS 2, LSCITS 3, LSCITS 4
Number of Credits 10
Part A+B
Teaching Spr/8
Closed Assessment [100%] TBA
Open Assessment [100%] Spr/8/Thu -> Spr/15/Wed
Feedback: Sum/4/Wed

Module Prerequisites

Prerequisite knowledge

Introduction to LSCITS

Workload

  • Lectures: 5 x 2hrs
  • Practicals: 6 x 1hr
  • Private Study: 43hrs
  • Assessment: 35hrs
  • Group Mini-Project: 6 x 1hr

The module teaching will be delivered over one week.

Assessment

Closed Assessment

  • , hours

Open Assessment

Open assessment

The assessment is through a multi-part report comprising:

Solutions to any two out of three questions from the following areas:

• Formal specification of a software system, identification of pre-conditions, post-conditions and invariants, and derivation of
JML assertions.
• Derivation of state transition graphs and NuSMV models, derivation of temporal logic formulas for safety and liveness
properties, and model checking with NuSMV
• Derivation of Markov chain models and their PRISM representation, derivation of dependability and performability properties,
and quantitative model cheeking with PRISM;

A reflection on/analysis of the group work during the week, including an evaluation of individual contribution to the group mini-project;

A high level discussion of how the techniques studies on the module (or a subset of them) could have helped prevent an infamous software bugs (to be chosen by each student from a given list

Formative Feedback

Oral feedback to indicate problem areas will be given in the practicals and problem classes. Written individual feedback will be returned after marking the open assessment.

Description

The module is intended as an introduction to Predictable Software Systems. It will cover key formal specification, modelling and verification techniques, and will illustrate their usage with real-world examples studied and analysed with state-of-the-art software tools. The focus will be on the use of formal methods for the specification and verification of software system properties including, safety, dependability, resource usage and performance. The students will have an opportunity to use various tools in practice. The module will provide some basic skills for those not studying the issue further, and a “platform” for those wishing to go into more detail in the specialist discipline.

The module aims:

  • Introducing the main methods for specification, modelling and verification that have been developed in recent years for establishing certain desirable properties of hardware and software systems;
  • Introducing model-checking and programming-by-contract software tools;
  • Considering examples, both small-scale ones for classroom demonstration and larger, real-world case studies in which verification has been successful;
  • Understanding the limitations of current tools, and how they may be overcome in the future.

Learning Outcomes

At the end of this module, students should:

  • Understand and explain the principles of specification, modelling and verification of hardware and software systems;
  • Explain the appliacation of programming by contract;
  • Understand the main classes of formal properties: safety, reachability, dependability, performability;
  • Explain and extend the application of the tools to the examples introduced;
  • Be able to select appropriate tools and use them to establish desirable properties of software systems;
  • Appreciate the limitations of current techniques and tools, such as the state explosion problem, and current efforts to overcome them.

Content

The module covers: formal specification and programming by contract, reactive systems and their models; temporal logic; model checking; a selection of tools; modelling formalisms; examples of systems (concurrent programs, communication protocols, embedded systems); verification of functional properties of systems (e.g., safety); probabilistic model checking; software verification; non-functional properties (dependability, reliability, performance); security and trust.

  1. Introduction to formal specfication and programming by contract. Propositional logic. Predicate logic. Z specification and Z schemas. Programming by contract. Examples of formal specification of system components and operations. Programming by contract with JML.
  2. Introduction to temporal logic model checking. Reactive systems and their transition system models. Temporal logics LTL and CTL. Model checking. Model checker NuSMV. Examples of simple protocols and safety/liveness properties.
  3. Model checking for distributed probabilistic systems, dependability and performance. Discrete and continuous Markov chains. Markov decision process models. The logic PCTL and PCTL extension with rewards. PCTL model checking.. Model checker PRISM. Examples simple systems and thier quatitative verification.
  4. Model checking for dependability and performance. Continuous-time Markov chains. The logic CSL and CSL extension with rewards. CSL Model checking. Examples of control systems and their quantitative verification (reliability, performance)

    Teaching Materials

    There is a wide range of material available on the web for each software tool, e.g.,
    http://nusmv.irst.itc.it/
    http://www.prismmodelchecker.org/
    http://www.jmlspecs.org/
    http://spivey.oriel.ox.ac.uk/mike/fuzz/

    Recommended Books

    Rating Author Title Publisher Year
    ** Michael Huth and Mark Ryan Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edition Cambridge University Press 2004
    ** Edmund M. Clarke, Orna Grumberg, Doron A. Peled Model Checking MIT Press 2000
    ** Beatrice Berard et al Systems and Software Verification: Model-Checking Techniques and Tools Springer 2001
    ++ J. Rutten, M. Kwiatkowska, G. Norman and D. Parker Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. Volume 23 of CRM Monograph Series. P. Panangaden and F. van Breugel (eds.) American Mathematical Society 2004
    ++ J Woodcock and J Davies Using Z: Specification, Refinement, and Proof. Prentice Hall 1996
    +
    +
    Back to top

    Last updated: 1st June 2011