UCSC - CMPE 276: Software Engineering

CMPE 276 - Software Engineering
Fall 2002

Instructor: Luca de Alfaro

4:00-5:45, TTh, Baskin 165

Office hours: Monday 1-2pm, Baskin 237A, or by appointment.
Instructor email: luca@soe.ucsc.edu

Syllabus, Lecture Notes, Homeworks, and Deadlines

Number	Date	Topic	Lecture Notes	Both Tracks	Tools Track	Project Track
1	9/19	Overview	lec01
2	9/24	Software process	lec02
3	9/26	Requirements and specification	lec03
4	10/1	UML	lec04
5	10/3	Design Patterns	lec05
6	10/8	Configuration management	lec06
7	10/10	Testing	lec07	Assigned reading: Statecharts, UML Statecharts	Homework 1 due	Informal discussion of project requirements
8	10/15	Project presentations				Project requirements presentation
9	10/17	Jannink: software development in startups	lec09
10	10/22	Software verification: Verisoft	lec10
11	10/24	Software model checking	lec11
12	10/29	Software model checking: BLAST Guest lecturer: Rupak Majumdar	lec12	Homework on Verisoft
13	10/31	Software model checking	lec13		Implementation and Verification of the Demarcation Protocol in Verisoft
14	11/5	Software model checking	lec14	Reading: Lecture notes, Chapter 1 (Postscript,PDF) Lecture notes, Chapter 2 (Postscript,PDF) CAV Book, Chapter 4: Symbolic Graph Representation (Postscript,PDF)
15	11/7	Dynamic analysis	lec15
16	11/12	Static analysis	lec16
17	11/14	Case studies	lec17		Homework 3
18	11/19	Protocol specification	lec18
19	11/21	Final project presentations				Final project presentation
20	11/26	Final Project presentations	lec20

Final Exam

Here is the Final Exam for the class. It is a take-home exam. Please return it at the latest on Wednesday December 4, 11am--5pm, to the instructor.

The course has two tracks: the project track, and the tools track.

Tools track

The students will apply software analysis tools to both assigned software, and to software of their own making. Moreover, the students will be asked to do homework on topics such as static analysis and software model checking. Some of the tools that will be presented are:

Tools Track - Grading

Midterm: 15%
Final: 25%
Homeworks: 60%

Project track

The students must work in teams (between 2 and 4 people), and must tackle a significant software development problem.

Project Track - Timeline

9/26: Propose project topics, and think at team members.
9/26: Project and team selection.
10/10 (tentative): Presentation of the requirements, and discussion. This will take place in a discussion session separate from class.
10/15: Project design presentation: specifications, proposed architecture. Required:

a presentation (about 20 minutes)
a report (about 10 pages)

requirements
team members
why it is useful
specifications
proposed breakdown in components, and component interfaces
discussion of main algorithms or problems to be solved

11/21: Project presentations. Demo of the project, discussion of the architectural and implementation choices. Documentation must be included!
11/21: The project is given to other teams, to evaluate usability, quality, documentation.
Dec 5: Reports from all teams requested (written design documents, and written notes on other team's projects).

Project Track - Grading

Midterm: 15%
Final: 25%
Project: 60%

Presentations: 10%
Project: 25%
Documentation and reports: 25%

Textbook

Pfleeger. Software Engineering. Prentice Hall, 2001.
(Advised, but not necessary.)

Readings

Software's Chronic Crisis, Scientific American, September 1994.
Nancy Leveson. Medical Devices: The Therac-25.ps pdf
Nancy Leveson. High-Pressure Steam Engines and Computer Software.ps pdf
Reports on the Loss of the Mars Polar Lander
Web tutorial (book, slides, etc) on the Z specification language.
David Harel. Statecharts. Science of Computer Programming 8 (1987), 231-274. North-Holland.
B.P. Douglass. UML Statecharts.
The Verisoft Manual.
POPL 1997 Paper on Verisoft.
R. Alur and T.A. Henzinger. Computer Aided Verification. The "CAV" book, posted with permission from the authors.
- Chapter 1: Reactive Modules (Postscript,PDF)
- Chapter 2: Invariant Verification (Postscript,PDF)
- Chapter 4: Symbolic Graph Representation (Postscript,PDF)
- Chapter 10: Hierarchical Verification (Postscript,PDF)
On program verification: lecures by G. Necula, UCB:
- Lecture 9
- Lecture 10
On BLAST:
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Lazy Abstraction.
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Gregoire Sutre, and Westley Weimer. Temporal-Safety Proofs for Systems Code.

Pointers

I was asked for an UML editor. Here is one: Poseidon for UML. I have not used it, and I would welcome other suggestions.

Luca de Alfaro

CMPE 276 - Software Engineering Fall 2002