Differences

This shows you the differences between two versions of the page.

--- course_outline [2007/07/31 19:53] – external edit 127.0.0.1
+++ course_outline [2009/05/07 17:23] (current) – jonathan
@@ Line 1: / Line 1: @@
 ====== Course Outline ======
-The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed:
+Programming Logic for Complex Systems This course covers program verification methods for a class of programs, commonly referred to as reactive programs. Reactive programs typically never terminate and are run in order to maintain some interaction with the environment. An adequate description of reactive systems must refer not only to initial and final states, but also to the ongoing behaviour as a (possibly infinite) sequence of states and events. The purpose of this course is to investigate the use of logical calculi for the **specification**, **design** and **verification** of reactive systems. Topics include: modelling of discrete event systems, semantics of real-time languages, logical and discrete calculi (e.g. temporal logic) for specifying and verifying safety, liveness, deadlock, priority and fairness properties of reactive programs, and prolog tools for automating verification
-===== Week 1 =====
+Lectures are in the Software Engineering lab CSE2056. The workstations are equipped with the Rodin (Event-B ) and Spin toolsets. Interspersed with the lectures, you will be asked to do small developments and proofs.
-Your notes here.
-===== Week 2 =====
-===== Midterm =====
-===== Drop Deadline =====
-===== Week 13 =====
-===== Final Exam =====
+  * User Requirements Documents , System Specifications and Models
+  *Introduction to formal methods
+  *Example of a concurrent system: controlling cars on a bridge (Event-B)
+  *Spin, Linear Time Temporal Logic and concurrency
+  *Mathematical Language and Proofs (Event-B)
+  *Sequential Program Development & Proofs.
+  *Two guest lectures by Albert Lai on Predicative Programming and the PVS theorem prover
+  *Example: File Transfer Protocol
+  *Wrap-up:  Science, Mathematical Models, Prediction and Engineering