| ______________________________________________ Contents
|
Sections and Locations:
| Section | Instructor | Time | Location |
| Lec A1 | Hoover | TR 09:30-10:50 | CSC B 41 |
Instructor:
| Instructor | Office | Web | |
| Jim Hoover | Athabasca Hall 308 | http://www.cs.ualberta.ca/~hoover | hoover@cs.ualberta.ca |
Contact:
The best way to contact me outside of the lecture is via email. In general I will not be having regularly scheduled office hours, but can answer questions via email, or arrange appointments as appropriate. The use of email is the most efficient use of your time and mine.
The course home page is http://www.cs.ualberta.ca/~hoover/cmput660. We do not have a newsgroup.
This course is about the relationship between the relatively fuzzy world of software architecture, and the relatively precise world of formal methods.
Software Architeture has been called the study of boxes and lines. More precise is the Bass, Clements, and Kazman definition: The software architectue of a progam or computing system is the structure or structures of the system, which comprise software components, the externally visible properties of those components, and the relationships among them.
For the most part, software architecture is informal in the sense that it is difficult to assign precise mathematical meaning to the graphical or textual descriptions of the organization of a system.
On the other hand, for machine models of computation, and for procedural and functional languages, it is possible to provide a reasonably precise semantics which makes it possible to reason about the properties of machines and programs. We do know how to reason about programs (but with OO being a notable difficulty). However the cost of formal reasoning is high, with ratios of proof length to program length on the order of 100 to 1 not being unusual.
So the dilemma of the computing scientist who wants to be precise is that we can only reason about rather small artifacts, but since we are reasonably good at building small artifacts such precise reasoning is not as important!
On the other hand, with complex systems the serious errors tend to be at the architecture level, such as the interaction of two complex subsystems. So it would seem that software architecture is a natural area in which to apply formal methods, if only we had something precise to reason about!
In this course the question we want to examine is:
Our slogan is:
This is very much a research course, so do not expect elegant polished results, but rather expect to be confronted by vague ideas, blind alleys, and partial progress. Students will be expected to participate in this process.
I am assuming that students in this course have a reasonably good background in either
In the first class you will be asked to complete a background quiz. If you find this quiz difficult, then you may be unprepared for this course. The quiz is at quiz.htm.
There is no specific text for this course, much of what we will study will be based on recent research.
The current list of assigned readings relevant to the lectures is:
Other references that are worth reading:
Software and links:
Distributions:
/usr/tees/cshome/hoover/cmput660/NuSMV-2.3.1/usr/tees/cshome/hoover/cmput660/binstonyplain.cs.ualberta.ca.
There will be 2 small assignments, and a larger (but not massive) course project. The details of these will be determined over time. Part of Assignment 1 will be to review someone elses assignment.
Assignment 1 - Due ?? via email
See assig1.htm
Assignment 2 - Due ?? via email
Project - Due ??
There are no examinations in this course. Your final mark will be based on the assignments, which may involve presentations and class participation.
| Small Assignment 1 | 20% |
| Small Assignment 2 | 25% |
| Project | 40% |
| Performance as a referee | 15% |
As part of the evaluation process, each of your assignments and papers will be read by two other students in the class. This will introduce you to the academic peer-review process. Although it may be strange at first to read and evaluate your classmates' work, this is what happens in the real world of research, so you might as well be exposed to this process now. Also, it is very enlightening to see how others attack the same problem. Your performance as a referee will also be evaluated, and contributes to your final mark.
Your final grade will be based on my interpretation of the grading system as defined in Section 23.4 of the Academic Regulations. I do not use a pre-defined function of your final mark to compute your final grade, but instead use my judgement of how the class final marks reflect mastery of the course material. I believe that this produces a fair evaluation, and my extensive past experience supports this.
Here is roughly how I plan to interpret the descriptors associated with the letter grades for graduate students.
| Letter | Descriptor | Interpretation |
| A-, A, A+ | Excellent | Consistently original thinking that extends the material, demonstrated depth and breadth in the material, ability to integrate material with other subjects, ability to analyse and synthesize material at various levels of abstraction. |
| B, B+ | Good | Like an A, but not consistent over time, or weak in a specific area. |
| C+, B- | Satisfactory | Understanding of the core material but not its subtlties, can apply it to simple situations, evidence that the material has changed the way of thinking. |
| F, D, D+, C-, C | Failure | Little evidence of understanding of even the surface issues, poor analysis and synthesis, inability to apply the material. |
Here is the conversion table we use at the U of A for computing your GPA:
| Letter | A+ | A | A- | B+ | B | B- | C+ | C | C- | D+ | D | F |
| GPV | 4.0 | 4.0 | 3.7 | 3.3 | 3.0 | 2.7 | 2.3 | 2.0 | 1.7 | 1.3 | 1.0 | 0.0 |
I assume that students are familiar with the University Regulations and Information for Students, especially with the Code of Student Behavior (Section 26 of the UofA Calendar).
Unless otherwise indicated, assignments must be done individually. Of course, given the nature of this material, you can expect that multi-person assignments will be permitted.
I assume that students are familiar with how to write a scholarly term-paper, complete with proper references and citations. Note that plagiarism is a serious academic offense and will not be tolerated. When in doubt about whether something is legal or not, consult with me first to avoid problems later.
To refresh your understanding of the concept of plagiarism, please look at the following, google generated, sample of sites:
Special Services: Students who require accommodations in this course due to a disability affecting mobility, vision, hearing, learning, or mental or physical health are advised to discuss their needs with Specialized Support and Disability Services, 2-800 Students' Union Building, 492-2281 (phone) or 492-7269 (TTY).
Contact Jim Hoover, hoover@cs.ualberta.ca, about problems with or suggestions about this document. }
| Copyright © 2002, University of Alberta. This document was produced using the Apalon markup language, developed by the Software Engineering Research Lab, Dept. of Computing Science, U of A. Apalon is implemented in Perl, http://www.perl.org. Every computing scientist should know Perl. |