start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revision | Last revisionBoth sides next revision | ||
| start [2016/04/19 22:16] – jonathan | start [2016/04/19 22:16] – jonathan | ||
|---|---|---|---|
| Line 60: | Line 60: | ||
| 1. High-level state/event models and proof rules for invariant preservation | 1. High-level state/event models and proof rules for invariant preservation | ||
| + | |||
| 2. Refining a system and proving that the refinement preserves correctness | 2. Refining a system and proving that the refinement preserves correctness | ||
| + | |||
| 3. Proving convergence and absence of deadlock | 3. Proving convergence and absence of deadlock | ||
| + | |||
| 4. Overview of system modelling constructs and proof rules for correctness in a reactive system | 4. Overview of system modelling constructs and proof rules for correctness in a reactive system | ||
| + | |||
| 5. Design of a distributed systems illustrated with an ftp protocol | 5. Design of a distributed systems illustrated with an ftp protocol | ||
| + | |||
| 6. Anticipated events in high-level models for convergence | 6. Anticipated events in high-level models for convergence | ||
| + | |||
| 7. Use of contexts to develop relevant theories such as parity | 7. Use of contexts to develop relevant theories such as parity | ||
| + | |||
| 8. Nondeterministic systems and associated safety invariant proof rules | 8. Nondeterministic systems and associated safety invariant proof rules | ||
| + | |||
| 9. Design of sequential programs with correction by construction via refinement rules | 9. Design of sequential programs with correction by construction via refinement rules | ||
| + | |||
| 10. Hoare logic and weakest preconditions for program design and its use in a variety of developments | 10. Hoare logic and weakest preconditions for program design and its use in a variety of developments | ||
| + | |||
| 11. Methods for systematic development of correct-by-construction of reactive systems, illustrated with a train system | 11. Methods for systematic development of correct-by-construction of reactive systems, illustrated with a train system | ||
| + | |||
| 12. Thinking before Programming using Lamport’s TLA+ specification method | 12. Thinking before Programming using Lamport’s TLA+ specification method | ||
start.txt · Last modified: 2016/04/19 22:22 by jonathan