COMP2214 Advanced Software Modelling and Design

Collection items

[img] [img]
COMP2214 - Lecture 00 - Introduction
Introduction to Advanced Software Modelling & Design

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 01 - Proof-based verification in Event-B
Proof-based Verification in Event-B

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 02 - Deductive Proof (Propositional Logic)
- Constructing Proof Trees - Inference Rules - Applying inference rules backwardly to construct proof trees

Shared with the University by
Dr Son Hoang
[img] [img]
[img] [img]
COMP2214 - Lecture 05 - Tree File
- Tree file system - Transitive Closure

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 04 - Set Theory
A refresher on Set Theory

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 06 - Reachability in Transition System
Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 07 - Debugging Models with Proof and Judgement
Debugging Models with Proof and Judgement - Strengthen Guards - Modify Actions - Strengthen Invariants - Weaken Invariants

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Coursework descriptions 2020-21
Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 08 - Extension Refinement
- Abstraction & Refinement - Extension Refinement

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Tutorial 04 - Fixing models using failing proofs
Fixing models using failing proofs

Shared with the University by
Dr Son Hoang
[img] [img]
[img] [img]
COMP2214 - Lecture 10 - Data Refinement
Shared with the University by
Dr Son Hoang
[img] [img]
[img] [img]
COMP2214 - Lecture 11 - An Elevator System
Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 12 - Convergence and Deadlock-freeness
Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Lecture 13 - Contracts
Slides from Prof Michael Butler

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 16 - Event-B to Dafny
Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Lecture 14 - Loops
Reasoning about looping programs

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 15 - Verification in Dafny
Verification in Dafny

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Tutorial 7 - Verification with Dafny (part 2)
Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Tutorial 6 - Verification with Dafny (part 1)
Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Lecture 17 - System Theoretic Process Analysis
Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Lecture 18 - Requirements Engineering
Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Lecture 19 - Safety-Critical Systems
Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Lecture 20 - Security Engineering
Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 21 - Revision
Revision lecture

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 15 - Introduction to Ada
Introduction to Ada programming language

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Lecture 16 - Introduction to SPARK
Introductory slides on SPARK

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 Lecture - Event-B to SPARK
This lecture about data refinement from Event-B models and generating SPARK/Ada from the model

Shared with the University by
Dr Son Hoang
[img]
COMP2214 - Tutorial 00 - Introduction to the Rodin Platform
Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Tutorial 01 - Deductive Proof (Propositional Logic)
Exercises for Propositional Logic Proof in Rodin Platform

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Tutorial 02 - Deductive Proof (Predicate Logic and Set Theory)
Exercises for Predicate Logic and Set Theory Proof in Rodin Platform

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Tutorial 03 - Model a Routing System
Model a Routing System using transitive closure

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Problem Class 6 - Hoare Logic
Exercises on Hoare Logic

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Problem Class 7 - Hoare Logic in SPARK
Exercises on Hoare Logic in SPARK - Flow analysis - Pre-/Post-conditions - Loops: Invariants, Variants

Shared with the University by
Dr Son Hoang
[img] [img]
COMP2214 - Problem Class 8 - Elevator System in SPARK
Exercise using the Elevator System in SPARK

Shared with the University by
Dr Son Hoang

COMP2214 Advanced Software Modelling and Design

Actions (login required)

View Item View Item

Toolbox

There are no actions available for this resource.