|Taken By||LSCITS 1, LSCITS 2, LSCITS 3, LSCITS 4|
|Number of Credits||10|
[100%] Spr/8/Thu -> Spr/15/Wed
Introduction to LSCITS
The module teaching will be delivered over one week.
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
• 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:
At the end of this module, students should:
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.
There is a wide range of material available on the web for each software tool, e.g.,
|**||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: 1st June 2011