course_outline
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| course_outline [2013/01/31 02:48] – jonathan | 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: | ||
| - | ===== Specification and Refinement | + | ===== Reactive systems |
| * Read the Rodin Users handbook up to and including Section 2.5.2. | * Read the Rodin Users handbook up to and including Section 2.5.2. | ||
| Line 19: | Line 19: | ||
| * Controller events and Environment events | * Controller events and Environment events | ||
| - | ===== FTP protocol ===== | + | ===== Distributed system -- FTP protocol ===== |
| Chapter 4 of textbook -- A simple File Transfer Protocol (FTP). | Chapter 4 of textbook -- A simple File Transfer Protocol (FTP). | ||
| Line 38: | Line 38: | ||
| **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, | **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.1359600518.txt.gz · Last modified: 2013/01/31 02:48 by jonathan