Practical System Modelling using Discrete Mathematics

Abstract

This course introduces ways of specifying, designing and implementing computerized systems so that the outcome will be correct by construction. It is essentially made of a large number of examples explaining how to write and prove formal models of discrete systems using abstraction and refinement.

Objective

The main goal of this course is to provide students with some knowledge on: - Modelling of discrete transition systems - Mathematical techniques to be used to construct and validate such models - Many different areas where such modeling techniques can be used

Content

The course is organized around examples. General topics are introduced together with the examples and summarized at the end of each example presentation. 1. Introduction: What is modelling for. The importance of the Requirement Document to be written before starting modelling. How to write such a document 2. Example: Managing cars on a narrow bridge 3. Example: File transfer protocol 4. Example: Leader election on a ring-shaped network 5. Example: Process synchronization on a tree-shaped network 6. Example: Mobile object routing protocol 7. Example: The IEEE-1394 leader election protocol 8. Refresher in First Order Predicate Calculus and set theory with a special emphasis on proof construction (manual proofs as well as proofs performed with a mechanized prover) 9. Example: Sequential program development. Many examples will be presented under this header (in particular the development of programs dealing with pointers) 10. Example: Concurrent program development of linear queue services 11. Example: Hardware development of a traffic light controller 12. Example: Complete system development. A door management controller 13. Example: Complete system development: A mechanical press controller

Resources