|LIC||Ken Robinson||kenr||K17 208||9385 4045|
|Tutor||Xiao Di Guanfirstname.lastname@example.org|
|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|
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.
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
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.
The assessment for this course consists of:
|1 small assignment||5%|
|2 medium assignments||15%|
|1 medium assignment||20%|
All assignments will be submitted using the cse give command. Instructions for each assignment will be given in the assignment specification.
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:
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!
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.
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.
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|
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.