course_outline
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
| course_outline [2007/07/31 19:53] – external edit 127.0.0.1 | course_outline [2013/04/07 15:52] (current) – jonathan | ||
|---|---|---|---|
| Line 3: | Line 3: | ||
| 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: | ||
| - | ===== Week 1 ===== | + | ===== Reactive systems via the bridge example |
| - | Your notes here. | + | * Read the Rodin Users handbook up to and including Section 2.5.2. |
| - | ===== Week 2 ===== | + | * Bridge controller (reactive systems) [[http:// |
| + | *Required readings: Read Chapters 1 and 2 from the suggested text [[http:// | ||
| - | ===== Midterm ===== | + | Topics covered by the bridge controller include |
| + | * Initial models and Proof rules for invariant preservation | ||
| + | * Refinement/ | ||
| + | * Proof rules for refinement | ||
| + | * Deadlock prevention and relative deadlock | ||
| + | * Divergence, Convergent events and variants | ||
| + | * Proof rules including SIM | ||
| + | * Controller events and Environment events | ||
| - | ===== Drop Deadline | + | ===== Distributed system -- FTP protocol |
| - | ===== Week 13 ===== | + | Chapter 4 of textbook -- A simple File Transfer Protocol (FTP). |
| + | * [[http:// | ||
| - | ===== Final Exam ===== | + | In the previous example, the program was **reactive** (i.e. it had to control an external situation such as cars on a bridge). This chapter deals with a protocol used on a computer network to transfer data from a sender to a receiver. The example will also allow us to extend our mathematical language with sets, functions and relations. As usual we will start with a requirements document. The initial model tells us what the protocol is supposed to achieve without telling us how to achieve it; how to achieve it will be dealt with in succesive refinements. Note that the model presented in the slides (using the notion of an **anticipated** event) is different than that of the textbook. |
| + | In the second refinement in the [[http:// | ||
| + | In the third and final refinement we add a parity bit. The distributed ftp protocol is now ready to be implemented in code (how would you write the program?) with a guarantee that it will terminate with the file properly transmitted from the sender to the receiver. Lab: prove the parity bit theorem. | ||
| + | |||
| + | Try a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem might be hard to prove. The suggestion is to first do the proof manually, which then makes it easier to do in Rodin. Using this approach, we were able to derive a Lemma that was helpful in the Rodin proof. | ||
| + | |||
| + | |||
| + | **Do all the lab exercises in preparation for the latest | ||
| + | |||
| + | |||
| + | **Required reading**: all of chapter IV and chapter V (Event-B proof obligation rules). Injections, surjections and bijections in Event-B. Review: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, | ||
| + | |||
| + | ===== Sequential Program Development ===== | ||
| + | |||
| + | [[http:// | ||
| + | |||
| + | We study two examples of the development of programs using loops by Dijkstra using the Hoare notation and the proof obligations for loop invariants and variants. Separation of concerns via partial correctness and termination arguments. Weakest preconditions and the wp-axiom for assignment. See also the slides " | ||
| + | |||
| + | ===== Using Relations ===== | ||
| + | |||
| + | We develop a phone book example by developing a mathematical model from informal E/ | ||
| + | |||
| + | ===== More systems ===== | ||
| + | |||
| + | in the last two weeks of class we studied a train system and an EHealth medication system. | ||
| + | |||
| + | For the EHealth system the requirements were: | ||
| + | *E1: a set of doctors prescribes drugs to a set of patients | ||
| + | *E2: there exists pairs of drugs that when taken together have undesirable interactions | ||
| + | *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: | ||
course_outline.1185911597.txt.gz · Last modified: 2013/01/08 04:45 (external edit)