Formal Specification Techniques -- CAS 707
CAS 707: Formal Specification Techniques
Winter 2007
Organization Meeting: 1:30am Tuesday January 9th in ITB/222
Instructor:
Course Web Page:
- http://www.cas.mcmaster.ca/~sartipi/course/cas707/w07/
Course Objectives:
- Software requirement analysis and specification is considered as an increasingly important activity within the software development process that has direct impact on the quality, maintenance, economic and success of the developed system. In this context, formal specification aims at describing the software requirements precisely and thoroughly using a collection of techniques, languages and tools that capture the abstract features of the system and allow us to verify and reason about the properties of the software before proceeding with the design and implementation. This will save a large amount of time and energy in producing the proper system. In this course, we will study different types of formal specification methods to provide an appreciation of the variety and power of different techniques using a case study throughout the course. The students will have the opportunity to exercise with selected formal specification tools in a course project.
Lectures:
Tuesdays: 1:30pm - 4:30pm in ITB/222
- One lecture per week. In the first part of each lecture, the instructor will discuss a scheduled subject with emphasis on the fundamental issues and problems to be addressed. In the second part of the lecture the students will present specific approaches in technical papers found in the related literature and will moderate the follow up discussions on the presented approach.
Textbook and References:
Course Outline:
- State-based approaches
- Event based
approaches
- Algebraic specifications
- Petri nets
- Temporal logic
- Properties of programs
- Specification
- Verification
- Validation
Back to TOP
Tentative Marking Scheme:
- Participation in class discussions: 10%
- Paper presentations: %30
- Project using a formal specification tool: 30%
- "Written exam" or "Technical paper": 30%
Resources for Formal Method Techniques
Class Presentation & Final Technical Paper ---- Instructions and Guidelines
- Class Presentation:
- Presentations are scheduled during the class sessions (see below)
- Presentation guidelines by professors at University of Waterloo
- Criteria for evaluation of your class presentation:
- Effectiveness of the presentation [30%]
- Quality of slides according to the presentation guideline above [20%]
- Number and quality of resources used for the presentation; at least 2 [20%]
- Timing: 50 minutes presentation including conclusion and question/answer [10%]
- Interaction with audience, such as: asking questions; making sure the audience follow the talk [10%]
- Critically evaluating the papers or the method you are presenting [10%]
- Final Technical Paper: (Due on Friday April 13)
Term Project:
Individual or group projects (in groups of 2 students) as follows:
- Software Requirement Specification (SRS) for two Systems as Project Case Studies:
- Formal specification:
- Select one of the above software systems. We should have almost equal number of groups for each system to learn both systems.
- Abstract away the details to some higher level that is appropriate for specifying with your formal method.
- Specify the systems using "Z" and "UML" specification techniques and their corresponding tools.
- For "Z" specification, you need to verify some of the major properties of the software system. (NOTE: announcement March 8, 2007).
- For restaurant system: "order-taker", "assembly", and "food-preparation" stations.
- For the ABM system, the whole system.
- For "UML" you need to specify the high-level requirements of the system using: "use-case diagram", "component diagram", "statecharts", "activity diagram", "sequence diagram", and "collaboration diagram". Also, specify the low-level requirements of each component using "class diagrams".
- Project deliverables:
- (Feb 13) Preliminary draft: plan, schedule, and task definition. [10%]
- (Feb 27) Hard copy of the Software Requirement Specification (SRS) document prepared according to the modified version of the IEEE SRS template. [40%]
- (Mar 20 -> Mar 27 (NEW) ) System specification using Z and UML tools and project presentation. [50%]
- (Mar 27 & Apr 3) Project presentations. See Week 12 (Mar 27) and Week 13 (Apr 3) for the presentation schedules.
- Web SVN:
- AWebSVN will be available to log the versions of your project.
- There will be a separate repository for each student, that can be accessed through: https://websvn.mcmaster.ca/cas707/
- Usernames and passwords are the same as the CAS Unix accounts.
Back to TOP
Course Materials: readings, and slides:
- Week 1 (Jan 9) :
- Organization Meeting: Tuesday January 9 at 1:30 in ITB/222
- Slides: .pdf
- Week 2 (Jan 16) :
-
Mathematical Fundamentals: Relations; Functions; Logical expressions; Quantifiers; Types; Sequences; Tuples [reading: chapter 3 Aho: .doc ;;;; .pdf]; [slides: .pdf].
- Slides from lectures on Software Engineering by: Mike Wooldridge [Propositional Logic: .pdf]; [Sets: .pdf]; [Functions: .pdf]; [First-Order Logic: .pdf]
- Introduction to Z schemas: [slides Z: .pdf]
- Week 3 (Jan 23) :
- Chapter 1: .doc
- Chapter 2: .doc
- By jin cai guo
- Introducing two software systems to be used for the course project. See project.
- Week 4 (Jan 30) :
- UML diagrams. In the first part of the class I will introduce different UML diagrams using case studies; and in the second part of the class a student will present a more challenging case study with emphasize on the more advanced UML properties.
- Chapter 6: UML: .doc
- UML Walk-through; [reading: .pdf]; [slides: .pdf]
- Project: specification of the restaurant system using UML.
- See the project definition above.
- Class presentation: Saba Aamir (UML) [slides: .pdf]
- Week 5 (Feb 6) :
- UML case studies from text book;
- Design Patterns; [reading: .doc]; [slides: .pdf]
- Statechart specification [reading: .pdf]; [slides: .ppt]
- Specification of the restaurant system [reading: .pdf]
- Class presentation: Wen Yu (UML2 and OCL) [slides: .pdf]
- Week 6 (Feb 13) :
- B-method: chapters 3 & 4 [slides: .pdf ]
- Week 7 (Feb 20) :
- Week 8 (Feb 27) :
- Action systems: chapter 5 [slides: .pdf]
- Class presentation: John Carter (B-Method) [slides: .pdf]
- Class presentation: Dawei Wang (CSP) [slides: .pdf]
- Week 9 (Mar 6) :
- LOTOS: chapter 10 [slides: .pdf]
- Class presentation: Kedong Lin (LOTOS) [slides: .pdf]
- Class presentation: Donald Morgan (Temporal Logic and Model Checking) [slides: .pdf]
- Week 10 (Mar 13) :
- Petri-Nets: chapter 14 [slides: .pdf]
- Class presentation: Yusufu Munina (Petri-Nets) [slides: .pdf]
- Class presentation: Feng Xiao (Petri-Nets) [slides: .pdf]
- Week 11 (Mar 20) :
- SDL: class presentation by Fang Cao
(including case study in text book) [slides: .pdf]
- VHDL: class presentation by Ge Zhou (including case study in text book) [slides: .pdf]
- Week 12 (Mar 27) :
- Project submission: ABM/Restaurant system specification using Z and UML tools
- Alloy: class presentation by Yuan Zhu [slides: .pdf]
- See new information for writing Final Technical Paper above.
- Course Project presentations
| Saba Aamir & John Carter |
2:30 - 3:05 |
ABM |
| Don Morgan & Jincai Guo |
3:10 - 3:45 |
Restaurant |
- Week 13 (Apr 3) :
- Course Project presentations
-
| Kedong Lin & Yuan Zhu |
1:30 - 2:05 |
ABM/Restaurant |
| Fang Cao & Munina Yusufu & Wen Yu |
2:10 - 2:45 |
ABM/Restaurant |
| Feng Xiao & Dawei Wang & Ge Zhu |
3:00 - 3:35 |
ABM/Restaurant |
- Monday (Apr 16): Due time for "Final Technical Paper"
Back to TOP
Announcements:
- Check this web page regularly for announcements.
- (Mar 20) Due to requests from students, the deadline for the course project submission will be extended to next Tuesday March 27, in the beginning of the class.
- (Mar 17) Two postings: i) instructions and guidelines for writing "Final Technical Paper" posted above; ii) project presentation schedules: see Week 12 (Mar 27) and Week 13 (Apr 3) above.
- (Mar 8) Based on a discussion at the end of Tuesday's class with students, I noticed that
the CZT tool as Eclipse plug-in may be just an editor that allows you to specify
the Z-schemas in PDF format and not more.
Note that for the project, you need to verify and / or simulate your specification in Z.
Therefore, if the Eclipse plug-in is not enough you need to install the CZT version
that is introduced in the CZT home page:
http://czt.sourceforge.net/
As I mentioned on Tuesday, I will check the progress next week after the class.
Also see a paper on how to use CZT above.
- (Feb 1) More specification and "project marking scheme" have been posted above.
- (Jan 31) The criteria for evaluation of the presentations are posted above.
- (Jan 22)
Two software systems "Restaurant System" and "Automatic Banking Machine" for the course project have been posted above.
- (Jan 1) Happy New Year 2007!!
Back to TOP