CSSE4603/CSSE7032 Home Page
Models of Software Systems

School of Information Technology and Electrical Engineering

The University of Queensland

Lecturers

Peter Robinson - Room 316, Phone: 3365-3461, email: pjr@itee.uq.edu.au

Graeme Smith - Room 315, Phone: 3365-1624, email: smith@itee.uq.edu.au

Ian Hayes - Room 326, Phone: 3365-2386, email: ianh@itee.uq.edu.au

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.

Workplace (Occupational) Health & Safety (WH&S; OH&S) in ITEE

The School of ITEE takes its obligations to WH&S very seriously. WH&S is everybody's responsibility, both the School's and the students'. The School has worked to ensure that WH&S processes are effective and that assessments are kept up to date. Students must take the time to familiarise themselves with these procedures and assessments.

Before entering any ITEE lab, students must read the student edition of 'OH&S in the Laboratory'

    http://studenthelp.itee.uq.edu.au/ohs/

and complete the Safety Declaration Form to be found there. In addition, students must complete the 'Student OH&S Induction' on Blackboard. Blackboard is accessed by following the Blackboard 9 logon link at

    http://www.elearn.uq.edu.au/ or http://blackboard.elearning.uq.edu.au/webapps/portal/frameset.jsp

Other relevant information on WH&S in the School is to be found at

    http://www.itee.uq.edu.au/~whs/

including the links from that page to

    http://www.itee.uq.edu.au/~whs/Risk%20Assessment%20Register
    http://www.itee.uq.edu.au/~whs/Electrical%20Safety/

Students, please ensure, by reading the information just referenced and completing the OH&S Induction and Safety Declaration Form as appropriate, that you are an active participant in a safe learning environment.

Lectures for Week 1

You will soon be provided with DVDs containing all the lectures. In the meantime you can either download or watch online Lectures 1 and 2.

Lecture downloads or online

Project Groups

The group allocations for the three projects can be found here. Please let us know as soon as possible if there are any problems.

Please take the time to look at the peer evaluation form on the Blackboard site (Projects).

Examples

Example proof from 23/03/11 here.

Results

Results for homework and projects are here.

Lecturing and Reading Schedule

Week	Lectures	Readings	Assessment
1. 28/2	L1 - What is a model? L2 - Logic	Course profile [GWC10] Ch 1-3
2. 7/3	L3 - Proof techniques L4 - Sets, relations, functions	[GWC10] Ch 4,5 [GWC10] Ch 6	HW 1
3. 14/3	L5 - Sequences and induction L6 - State machine basics	[GWC10] Ch 7 [GWC10] Ch 8	HW 2
4. 21/3	L7 - State machine variations L8 - FSP and LTSA	[GWC10] Ch 9 [MK06] Ch 1-3	HW 3
5. 28/3	L9 - Reasoning about state machines L10, L10a - Lab on FSP and LTSA	[GWC10] Ch 9 no additional reading	HW 4
6. 4/4	L11 - Intro to Z L12 - Z Techniques	[Spi89] 40-44; [WD96] 11.1, 12.2 [PST96] Ch 6	P1 due HW 5
7. 11/4	L13 - Z Examples L14 - Refinement and abstraction	[HP99] [Spi89] 45-50; [WD96] 11.4,14,16.1	HW 6
8. 18/4	L17 - Intro to models of concurrency L18 - Modelling concurrency in FSP	[AS83] [MK06] Ch 1-3	HW 7 (due Thu)
25/4	Mid-semester break
9. 3/5	L19 - Modelling techniques (FSP) L20 - Reasoning about concurrency	[MK06] Ch 4-5 [MK06] Ch 6-7	P2 due HW 8
10. 9/5	L21 - Linear Temporal Logic L22a- LTL in FSP	[Katz96] Ch 6 [MK06] Ch 14	HW 9
11. 16/5	L22b - Model checking, Automatic Reasoning L25 - Introduction to Petri nets	no additional reading [Pet77]	HW 10
12. 23/5	L25a, L26 - Lab and Petri Nets L23 - FM in the real world	[CW96] [Ha87]; [MLPS97]	P3 due HW 11
13. 30/5	L29 - Review		HW 12
6/6	Study period
E1. 14/6	Exam period
E2. 20/6	Exam period

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.
[GWC10]	D. Garlan, J. Wing, and O. Celiku. 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.

Online Submission

Your homework and projects are to be submitted through the electronic submission system at http://submit.itee.uq.edu.au.

Please read http://submit.itee.uq.edu.au/student-guide.pdf for instructions on using electronic submission.

CSSE4603/CSSE7032 Home Page Models of Software Systems