User Tools

Site Tools


course_outline

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
course_outline [2016/04/19 22:21] jonathancourse_outline [2018/01/03 02:03] (current) jonathan
Line 2: Line 2:
  
 The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed: The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed:
 +
 +===== Introduction =====
 +
 +Use this small project to get started with Event-B and the Rodin tool
 +
 +  * {{:01-intro-bank.pdf|Simple Bank System}}. Introduction to Specification and Refinement. 
 +  * [[https://youtu.be/aROKK2HKhog|Video Presentation]]
 +
 +
  
 ===== Reactive systems: Bridge ===== ===== Reactive systems: Bridge =====
Line 56: Line 65:
  
 ===== TLA+ Thinking for Programmers ===== ===== TLA+ Thinking for Programmers =====
 +
 +[[http://lamport.azurewebsites.net/video/videos.html|TLA Videos]]
  
 See slides 11: Thinking for Programmers. Leslie Lamport's TLA+ specification tool, its use at Amazon and for MS/Xbox 360. Thinking for programmers. QuickSort at the algorithmic level as a divide and conquer algorithm rather than a program. The algorithm can be refined to a recursive implementation, an iterative implementation and a concurrent implementation. See slides 11: Thinking for Programmers. Leslie Lamport's TLA+ specification tool, its use at Amazon and for MS/Xbox 360. Thinking for programmers. QuickSort at the algorithmic level as a divide and conquer algorithm rather than a program. The algorithm can be refined to a recursive implementation, an iterative implementation and a concurrent implementation.
Line 67: Line 78:
 See slides 12. Method for systematic development correct-by-construction reactive systems. See slides 12. Method for systematic development correct-by-construction reactive systems.
  
 +===== Exam Preparation =====
 +
 +The following examples are unlikely to be on the exam. 
 +
 +Develop a phone book example by developing a mathematical model from informal E/R-descriptions. Relations, Functions and the override operator, relational image, relational inverse, domain and range restrictions and subtractions, and relational composition. 
  
  
-===== Grades =====  +Develop an Event-B project for an EHealth medication system.
  
-  [30%] Weekly quizzes. There will be about 8 weekly quizzes (almost every week). The first 2 quizzes each count 3%. The last 6 quizzes each count 4%. On condition that the Lab work is completedQuizzes will be based on the Labslectures and required readings of the preceding weeks. +For the EHealth system the requirements were: 
-  * [15%] LabTest after reading week+  *E1: a set of doctors prescribes drugs to a set of patients 
-  * [15%] Project (working in a team of no more than two students) +  *E2: there exists pairs of drugs that when taken together have undesirable interactions 
-  * [40%] Final exam+  *E3: Drug interaction is symmetric, i.e. if a drug interacts with anotherthen the reverse also applies 
 +  *R1: A doctor shall be capable of adding drugs to a patients’ prescription
 +  *R2: A doctor shall not prescribe two drugs that interact 
 +  *Goal:  minimize the number of undesirable interactions
  
-It is required that you attend and complete the work allocated in the weekly Lab session in preparation for the Quizzes, Labtest, Project and Exam. <hi> Labs must be completed by their due date in order for you to receive credit for the Quizzes</hi>  
course_outline.1461104516.txt.gz · Last modified: 2016/04/19 22:21 by jonathan