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/WedFeedback: Sum/4/Wed |

Introduction to LSCITS

- 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.

- , hours

- Spr/8/Thu -> Spr/15/Wed, uses electronic submission.
**Feedback:**Sum/4/Wed

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

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.

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.

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.

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.

- 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.
- 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.
- 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.
- 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 + + Last updated: 1

^{st}June 2011