COMP2111: System Modelling & Design
Organisation
| LIC | Ken Robinson | kenr | K17 208 | 9385 4045 |
| Tutor | Xiao Di Guan | xdg@cse.unsw.edu.au | ||
| Activity | Time(s) | Place | UNSW Grid | |
| Lecture | Mon 0900–1100 | Law Theatre G23 | K-FB-G23 | |
| Lecture | Wed 1200-1300 | Law Theatre G02 | K-FB-G02 | |
| Tutorial | Wed 1300-1400 | ASB 114 | K-E12-114 | |
| Tutorial | Wed 1400-1500 | ASB 114 | K-E12-114 | |
Course Information
Units of Credit
Assumed knowledge: set theory, logic, first-order predicate calculus from MATH1081; general mathematical concepts from MATH1131/1141; programming concepts from COMP1011 & COMP1021; requirements concepts from SENG1031. COMP2111 is a co-requisite for SENG2010 and a prerequisite for SENG2020.
Course philosophy and teaching strategies: this course will be taught using lectures, tutorials and assignments. The formal course content will be augmented with the Rodin EventB toolkit and lectures will make extensive use of the toolkit to develop solutions. Assignments are designed as both learning and assessment tools.
Course aims:
the basic aim is an understanding of requirements analysis; to understand how to
progress from an informal (written or spoken) requirements document to a clear
understanding of what the requirements entail, and from there a design. In
particular, this course demonstrates how rigorous modelling can be used —as it is
used in other engineering disciplines— to develop designs that satisfy the
requirements. Modelling is used to identify the events that are contained in
informal requirements. Events are described in terms of possible parameters,
the conditions under which the event may occur and what changes occur
to the system when the event occurs. EventB provides rigorous checking
of the consistency of a model, and the EventB toolset (Rodin) provides
animation for checking observed behaviour against the informally expressed
requirements;
to develop and increase an appreciation of and ability to use modelling during system
design; to develop ability to explain and reason about designs both formally
and informally; to understand formal semantics of constructs that enable a
rigorous modelling of system behaviour; to develop an understanding of proof
obligations and to develop some facility in discharging of proof obligations using
the theorem provers of the Rodin toolkit; to develop an understanding of
how designs can be developed and enriched through a rigorous process of
refinement.
Learning outcomes: students should be able to use the EventB concepts to specify a system; the model should be composed of machines, each machine consisting of a state constrained by a state invariant and a set of pre-conditioned operations. Students will be have varying capacities to take the specification through refinement to an implementation and to verify such a development by discharging proof obligations. Students should be able to specify required behaviour —as distinct from implementation— using declarative and nondeterministic descriptions.
Assessment
The assessment for this course consists of:
| 1 small assignment | 5% |
| 2 medium assignments | 15% |
| 1 medium assignment | 20% |
| formal examination | 50% |
Assignment submission
All assignments will be submitted using the cse give command. Instructions for each assignment will be given in the assignment specification.
Academic Honesty and Plagiarism
What is Plagiarism?
Plagiarism is the presentation of the thoughts or work of another as ones own.
Copying assignments is unacceptable. Assignments will be checked. The penalties for copying range from receiving no marks for the assignment, through receiving a mark of 00 FL for the course, to expulsion from UNSW (for repeat offenders). Allowing someone to copy your work counts as plagiarism, even if you can prove that it is your work.
Further details of the School plagiarism policy can be found here. (You acknowledged receipt of these rules when you obtained your CSE computer account, and the link above is for your convenience so that you can review the rules now.)
We are aware that a lot of learning takes place in student discussion, and don’t wish to discourage that activity. However, it is important, for both those helping others and those being helped, not to provide/accept any assignment code in writing, as this is apt to be used exactly as is, and lead to plagiarism penalties for both the supplier and the copier of the codes. Write something on a piece of paper, by all means, but tear it up/take it away when the discussion is over.
In brief, and for the purposes of this course, plagiarism includes copying or obtaining all, or a substantial part, of the material for your assignment, whether programming language code, or written or graphical report material, without written acknowledgement in your assignment from:
- a location on the Internet;
- a book, article or other written document (whether published or unpublished) whether electronic or on paper or other medium;
- another student, whether in your class or another class;
- a non-student (e.g. from someone who writes assignments for money)
Note that if you copy code or other material from any source then the marks you get will be at the marker’s discretion, and will reflect the marker’s perception of the amount of work you put into finding and/or adapting the code, and the degree to which you understand the code.
Note also that there is a big difference between being able to understand someone else’s solution, and developing a solution yourself. A software engineer has to be able to develop solutions from scratch. Assignments provide opportunities for you to develop the skills necessary to develop your own solutions. Use these opportunities!
Resources for students
- System Modelling & Design Using EventB
- by Ken Robinson. The book is currently being written and copies will be available (as a PDF) during the semester. Feedback from students is encouraged and will be very welcome.
- Modelling in EventB
- System and Software Engineering by Jean-Raymond Abrial —the creator of EventB— published by Cambridge University Press.
- lecture notes
- Extensive lecture notes will be available on the class website. Also the book System Modelling & Design available on the class website.
- Rodin
- The Rodin toolkit provides comprehensive assistance for the definition and testing of models in EventB. It is implemented as a plugin for the Eclipse platform. The toolkit runs on Linux, Mac OS X and Windows operating systems. Use of the toolkit is an integral part of this course.
Course quality
The major course survey that the University takes note of is the CATEI (Course and Teaching Evaluation and Improvement) survey which is conducted at the end of the semester, however direct feedback to Ken Robinson is encouraged, as it is usually more effective in correcting any problems or misunderstandings.
Course administration
This information and all other course information will be installed in the course WWW page.
Communication on this course will be done either through explicit messages in the WWW page or through e-mail. All course e-mail will be stored in the course page. You are encouraged to consult the course page for information, or to use e-mail directly to the lecturer to enquire about any aspect of the course.
Brief outline
This course is concerned with the rigorous modelling of (software) systems using the B Method, or B. This will cover:
| modelling and design | what are they? |
| rigorous specification | set theory and logic |
| mathematical toolkit | set theory and logic |
| contexts | static environment in which events are embedded |
| events | general concept of discrete event |
| guards | conditions for an event to be enabled |
| semantics | generalized substitution semantics |
| verification of model properties | proof obligations |
| discharging proof obligations | use of prover |
| animation | validating a specification |
| refinement | enrichment of a design by refinement |
| structuring developments | layering of models |
| using Rodin | |
| documentation | |
Assignments
This course will use small and medium assignments to develop competence in the use of Event B for modelling small systems and also in the use of the Rodin as a development tool. These assignments may be unusual in the computing context by virtue of their size and deadlines.
The 2 small assignments have short deadlines, and the following medium assignments have 4-week deadlines.