CSSE4603/CSSE7032 Home Page
Models of Software Systems
School of Information Technology and Electrical Engineering
The University of Queensland
Lecturers
Paul Strooper - Room 324, Phone: 3365-1628, email: pstroop@itee.uq.edu.auPeter Robinson - Room 316, Phone: 3365-3461, email: pjr@itee.uq.edu.au
Results for 2009
The following link provides you with access to your results recorded for this semester (three projects and all homeworks, including the mark for the best 10 homeworks): results.csv. You will need your UQ student login and password to access your marks. Please let us know if there are any problems.
Link to UQ Blackboard website
The course Blackboard site will be used for posting announcements and electronic copies of all handouts. You can access the course Blackboard site via the UQ Blackboard login. Note that only students enrolled in CSSE4603 or CSSE7032 will have access to the course site.
Lecturing and Reading Schedule
|
Week |
Lectures |
Readings |
Assessment |
|
1. 2/3 |
L1 - What is a model? L2 - Logic |
Course profile [GWCK08] Ch 1,2; [WL88] pg 1-13 |
HW 1 |
|
2. 9/3 |
L3 - Proof techniques L4 - Sets, relations, functions |
[GWCK08] Ch 4,5 [GWCK08] Ch 6 |
HW 2 |
|
3. 16/3 |
L5 - Sequences and induction L6 - State machine basics |
[GWCK08] Ch 7 [GWCK08] Ch 8 |
HW 3 |
|
4. 23/3 |
L7 - State machine variations L8 - Reasoning about state machines |
[GWCK08] Ch 9 [GWCK08] Ch 10 |
HW 4 |
|
5. 30/3 |
L10 - Intro to Z L11 - Z Techniques |
[Spi89] 40-44; [WD96] 11.1, 12.2 [PST96] Ch 6 |
HW 5 |
|
6. 6/4 |
L12 - Z Examples L14 - Refinement and abstraction |
[HP99] [Spi89] 45-50; [WD96] 11.4,14,16.1 |
P1 due HW 6 |
|
13/4 |
Mid-semester break |
||
|
7. 20/4 |
L15 - Intro to models of concurrency L16 - Modelling concurrency in FSP |
[AS83] [MK06] Ch 1-3 |
HW 7 |
|
8. 27/4 |
L17 - Modelling techniques (FSP) L18 - Reasoning about concurrency |
[MK06] Ch 4-5 [MK06] Ch 6-7 |
HW 8 |
|
9. 4/5 |
L20 - Linear Temporal Logic New lec - LTL in FSP |
[Katz96] Ch 6 [MK06] Ch 14 |
P2 due HW 9 |
|
10. 11/5 |
L23 - Model checking Supp lec - Introduction to Petri nets |
no additional reading [Pet77] |
HW 10 |
|
11. 18/5 |
L25 - FM in the real world L26 - Statecharts and other models |
[CW96] [Ha87]; [MLPS97] |
HW 11 |
|
12. 25/5 |
L27 - UML 1 L28 - UML 2 |
[RJB99] pg 25-39 [Ha87] |
P3 due HW 12 |
|
13. 1/6 |
L29 - Review |
|
HW 13 |
|
8/6 |
Study period |
||
|
E1. 15/6 |
Exam period |
||
|
E2. 22/6 |
|||
Readings
|
[AS83] |
G.R. Andrews and F.B. Schneider. Concepts and Notations for Concurrent Programming. Computing Surveys, 15(1):3-43, March 1983. |
|
[CW96] |
E.M. Clarke and J.M. Wing. Report by the Working Group on Formal Methods for the ACM Workshop on Strategic Directions in Computing Research. Computing Surveys, 28(4): 626-643, 1996. |
|
[GWCK08] |
D. Garlan, J. Wing, O. Celiku, and D. Kroening. Models of Software Systems. Draft chapters from a book. |
|
[Ha87] |
D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987. |
|
[HP99] |
V. Harvey and P. Place. FAA En Route Resectorization—A Formal Specification. Unpublished manuscript, September 1999. |
|
[Katz96] |
S. Katz. Temporal Logic. Draft chapter of book, 1996. |
|
[MK06] |
J. Magee and J. Kramer. Concurrency - State Models and Java Programs, second edition. John Wiley & Sons, 2006. |
|
[MLPS97] |
E. Mikk, Y. Lakhnech, C. Petersohn, and M. Siegal. On Formal Semantics of Statecharts as Supported by STATEMATE. In Proceedings of the 2nd BCS-FACS Northern Formal Methods Workshop, 1997. |
|
[Pet77] |
J.L. Peterson, Petri Nets. Computing Surveys, 3(9):223-252, 1977. |
|
[PST96] |
B. Potter, J. Sinclair, and D. Till. An Introduction to Formal Specification and Z, second edition, Prentice-Hall International, 1996. |
|
[RJB99] |
J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Manual. Addison Wesley, 1999. |
|
[Spi89] |
J.M. Spivey. An Introduction to Z and Formal Specification. Software Engineering Journal, 40-50, 1989. |
|
[WD96] |
J. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice-Hall International, 1996. |
|
[WL88] |
J. Woodcock and M. Loomis. Software Engineering Mathematics. Addison Wesley, 1988. |