CAS756: Advanced Topics in Formal Methods and Software Architecture


Advanced Topics in Formal Methods and Software Architecture

Winter 2015

Course Outline

Created: 8 January 2015

Note: This course outline contains important information that may affect your grade. You should retain it throughout the semester as you will be assumed to be familiar with the rules specified in this document.

Instructor: Dr Tom Maibaum and Zinovy Diskin, Sahar Kokaly

Office: ITB 159

Extension: 26627




Lectures: Wed @ 2:30-5:20 in ITB222

Calendar Description

Formal specification methods. Requirements specifications. Fail-safe systems. Verification of safety critical applications. Systematic testing. Specification and design of concurrent, multi-process and distributed systems.


“The mission of this course is to give students an understanding of the foundations of Model Driven Engineering, specifically of the model management aspects of the approach”


Part I: Introduction to software architecture/design/design patterns and formal methods in software engineering.

Part II: Introduction to Model Driven Engineering (Models, Metamodels, Mappings, Transformations and other operations, Megamodeling,  Model Management, etc).

Part III: Introduction to Categories/Kleisli Mappings/Tiling

Part IV: Mapping-Aware Model Management

Part V: Design Patterns for Model Management


Design Pattern 1: Models

Design Pattern 2: Model Mappings

Design Pattern 3: Model Overlap


Design Pattern 4: Descriptive Views

Design Pattern 5: Prescriptive Views

Design Pattern 6: Model Transformation

Design Pattern 7: Bidirectional Transformation


Design Pattern 8: Model Merge (additive)

Design Pattern 9: Model Intersect (multiplicative)


Design Pattern 10: Composition/Tiling


Paper reviews (list of candidate papers will be supplied)


QueST vs. ETL - Students will write transformations for a predefined example using both techniques and write a summary of their experience using each technique.

Week by Week view:

Week 1: Jan 7 - Intro to formal methods for SE

Week 2: Jan 14 - Intro to MDE

Week 3: Jan 21 - Intro to Categories/Kleisli Mappings/Tiling

Week 4: Jan 28 - Mapping-Aware Model Management - Tutorial Slides Part 1

Week 5: Feb 4 - Mapping-Aware Model Management - Tutorial Slides Part 2

Week 6: Feb 11 - Design Patterns 1-3 + diagram predicates

Week 7: Feb 18 - No lecture (Reading Week)

Week 8: Feb 25 - Design Patterns 4-7

Week 9: Mar 4 - QueST + ETL tutorial (to initiate student projects)

Week 10: Mar 11 - Paper presentations

Week 11: Mar 18 - Design Patterns 8-9

Week 12: Mar 25 - Design Pattern 10 + diagram operations

Week 13: Apr 1 - Summary lecture (Mapping-Aware, Query-Structured and Constraints-Aware Framework)

Week 14: Apr 8 - Project Presentations (depending on number of students, might need Apr 15 as well)


Students are expected to read on average three papers each week, in advance of class. Over the course of the term, each student will also present two or three papers in class and will prepare reviews of five to seven additional papers. Finally, there will be a term project defined by the student.
The marking scheme is as follows:

Class participation


Paper reviews


Term project



Software Tools

Policy Statements

1. Missed deliverable or exam: You must submit appropriate documentation (e.g. note from physician) to the Associate Dean’s office. It is your responsibility to follow-up with the instructor. A zero will be entered for the missed work unless the instructor receives a Course of Action for Missed Work form delivered by the Associate Dean Office before submitting the final grades to the faculty.

2. Tutorials: The class will be split into two groups. Each group will have a two hour tutorial per week. Attendance at tutorials is compulsory. You MUST attend your assigned session of the tutorial. More information on the schedule and the organization of the tutorial will be posted very soon on the course website.

3. The instructor reserves the right to adjust the grades for a deliverable, or the final exam by decreasing every score by a fixed number of points.

4. The instructor reserves the right to increase by a fixed number of points the final scores of all the students who handed in all the deliverables and attended all the tutorial sessions (except if the student misses a tutorial for a justifiable reason).

5. The instructor reserves the right to assign extra grades for extra work done by willing students. However, the work subject to extra grades should be advertised during the lectures.

6. A remarking request of a deliverable is considered by the TAs and the instructor only if it is made within the two weeks that follow the return date of the majority of the concerned deliverable.

7. The instructor reserves the right to require a deferred exam to be oral.

8. No responsibility for loss of deliverables can be assumed by either the instructor or the Teaching Assistants. Keep copies of your own contributions to the project, your reports, and your email exchanges with your team members.

9. Calculators are not needed for this course and their use will not be permitted during exams.

10. The lectures will not necessary follow the order in which the topics are presented in the detailed course outline. Regular class attendance is required.

11. Significant study, reading, and group discussions outside of class and tutorials are required.

12. Suggestions on how to improve the course and the instructor’s teaching methods are always welcomed.

Important warning

The instructor and university reserve the right to modify elements of the course during the term. The university may change the dates and deadlines for any or all courses in extreme circumstances. If either type of modification becomes necessary, reasonable notice and communication with the students will be given with explanation and the opportunity to comment on changes. It is the responsibility of the student to check their McMaster email and course websites weekly during the term and to note any changes.


The Faculty of Engineering is concerned with ensuring an environment that is free of all adverse discrimination. If there is a problem that cannot be resolved by discussion among the persons concerned, individuals are reminded that they should contact their Chair, the Sexual Harassment Office of the Human Rights Consultant, as soon as possible.

Academic Integrity

Students are reminded that they should read and comply with the Statements on Academic Ethics and the Senate Resolutions on Academic Dishonesty as found in the Senate Policy Statements distributed at registrations and available in the Senate Office.

“Academic dishonesty consists of misrepresentation by deception or by other fraudulent means and can result in serious consequences, e.g., the grade of zero on an assignment, loss of credit with a notation on the transcript (notation reads: ”Grade of F assigned for academic dishonesty”), and/or suspension or expulsion from the university.”

It is your responsibility to understand what constitutes academic dishonesty. For information on the various kinds of academic dishonesty please refer to the Academic Integrity Policy, specifically Appendix 3, located at integrity.htm.

The following illustrates only three forms of academic dishonesty:

1.Plagiarism, e.g., the submission of work that is not one’s own or for which other credit has been obtained.

2.Improper collaboration in group work.

3.Copying or using unauthorized aids in tests and examinations.