Emil Sekerinski - CAS 703 Fall Term 2018/19

Schedule

  • September 7: First class, introductions
  • September 12: Modelling and Verification in Event-B, Butler's Lecture 1
  • Homework: Watch Abrial's Lecture 1; we will discuss it at the beginning of the class, be prepared for questions.
  • Homework: Install Rodin following the instructions below. If you have questions, bring them up at the next class, otherwise I assume that your installation works.
  • September 14: Modelling and Verification in Event-B, Butler's Lecture 2
  • September 19: Modelling and Verification in Event-B, Butler's Lecture 3
  • September 21: Rodin Tutorial
  • September 26:

Calendar Description

Formal specification methods. Requirements specifications. Fail-safe systems. Verification of safety critical applications. Systematic testing. Specification and design of concurrent, multi-process and distributed systems.

Prerequisites

Knowledge of discrete math, fluency in object-oriented programming, and willingness to study on your own. If you are not familiar with object-oriented programming, you should learn Eiffel, C#, or Java on your own, see recommendations below.

Outline

  • System modelling and analysis
  • Program correctness, modularization, exception handling, testing
  • Concurrent programming

Required Material

Further Reading

Assignments

  • Assignments cover system modelling, correctness, concurrency
  • Assignments are to be completed individually; they must constitute your own work and references to all used resources must be given. Details are announced with each assignment. See also the Academic Dishonesty policy below.

Project

  • Project topics will be suggested and will cover all aspects of the course. You have to choose a topic; in same cases, participats may have the same topic or similar topics. You can also propose a topic.
  • Projects must be completed individually; they must constitute your own work and references to all used resources must be given.
  • The project includes a presentation of 20 minutes. The project grade is determined by the understanding of the topic, coverage and difficulty of the topic, background knowledge, critical judgment, quality of slides (e.g. color, layout, animations), accompanying notes and materials (if applicable), demonstration (if applicable), clarity of explanation, convincingness of arguments, pace, language (each error gets a deduction)

Participation

  • This course lives from critical reflection on the material presented in class. All participants are expected to actively engage in discussions when the instructor and participants are presenting.
  • Attendance at all classes is mandatory. Someone who misses a class without explanation or a valid reason (e.g. University or health related) will be asked to withdraw from the course.

Academic Dishonesty

  • Academic dishonesty consists of misrepresentation of deception or by other fraudulent means and can result in serious consequences, e.g. the grade of zero on all assignments, loss of credit with a notation on the transcript (notation reads: "Grade of F is assigned for academic dishonesty"), and/or suspension or expulsion from the university.
  • It is your responsibility to understand what constitutes academic dishonesty. For information on the various kinds of academic dishonesty please refer to the Academic Integrity Policy, specifically Appendix 3. The following illustrates only three forms of academic dishonesty:
    • Submission of work that is fully or partly copied from someone else, or making your work available for copying to others.
    • Submission of work that has been fully or partly obtained from other sources like the Internet.
    • Copying or using unauthorized aids in tests and examinations.
  • All submitted assignments are always checked for similarities.
Emil Sekerinski