Differences

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

--- course_outline [2016/04/19 22:21] – jonathan
+++ course_outline [2018/01/03 02:01] – 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:
+===== 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]]
+<html>
+<iframe width="560" height="315" src="https://www.youtube.com/embed/videoseries?list=PLGoQo5eIwvcAmPWkiWVhzWR-Op-mYN9JK" frameborder="0" gesture="media" allow="encrypted-media" allowfullscreen></iframe>
+</html>
+<html>
+    <div id="player"></div>
+    <script>
+      // 2. This code loads the IFrame Player API code asynchronously.
+      var tag = document.createElement('script');
+      tag.src = "https://www.youtube.com/iframe_api";
+      var firstScriptTag = document.getElementsByTagName('script')[0];
+      firstScriptTag.parentNode.insertBefore(tag, firstScriptTag);
+      // 3. This function creates an <iframe> (and YouTube player)
+      //    after the API code downloads.
+      var player;
+      function onYouTubeIframeAPIReady() {
+        player = new YT.Player('player', {
+          height: '315',
+          width: '560',
+          videoId: 'aROKK2HKhog',
+          events: {
+            'onReady': onPlayerReady,
+            'onStateChange': onPlayerStateChange
+          }
+        });
+      }
+      // 4. The API will call this function when the video player is ready.
+      function onPlayerReady(event) {
+        event.target.playVideo();
+      }
+      // 5. The API calls this function when the player's state changes.
+      //    The function indicates that when playing a video (state=1),
+      //    the player should play for six seconds and then stop.
+      var done = false;
+      function onPlayerStateChange(event) {
+        if (event.data == YT.PlayerState.PLAYING && !done) {
+          setTimeout(stopVideo, 0);
+          done = true;
+        }
+      }
+      function stopVideo() {
+        player.stopVideo();
+      }
+    </script>
+</html>
 ===== Reactive systems: Bridge =====
@@ Line 56: / Line 115: @@
 ===== 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.
@@ Line 67: / Line 128: @@
 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 completed. Quizzes will be based on the Labs, lectures 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 another, then 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>