Model Driven Software Engineering

Lecturer: David Faitelson

  סטודנטים בקורס יכולים לראות את סיכום הציונים בתרגילים

שימו לב, מי שהגיש פחות מ-5 עבודות חייב לעשות את העבודה המסכמת בעצמו

Course Summary

Modeling is essential to every branch of engineering. A model is a simplified description of the system we intend to build. By analysing the model we can predict how the system will behave much more quickly and cheaply than actually building the system. In this course we will learn how to build and analyse models of software systems.

You can get an impression of what it all means by looking at the authentication example.

Syllabus

The course consists of two major parts. In the first part we will learn how to formalize requirements and specifications using the Z notation. In the second part we will learn how to automatically analyze formal models using the Alloy analyzer.

Part 1: Modeling Software systems with the Z language

     A mathematical toolkit of data types: 

          Definitions and sets, Relations and functions, Sequences and free types

     Structuring state and behavior: 

          Schemas, Schema operators, Modeling state and behaviour with schemas, Pre-condition analysis

Part 2: Automatic analysis with Alloy

     Overview of the Alloy modeling language, Modeling and analysing state and behaviour with Alloy

Readings

The first part of the course is based on the content of the book Using Z and its accompanying set of exercises, all of which are freely available on the Internet. In addition, you may find useful the book The way of Z by John Jacky. There are two copies of this book in the College library.

The second part of the course is based on the material that is available in the Alloy web site.

Read more about other sources of information

About the tools

We will write the Z models as LaTeX documents, so it is important that you will make yourself familiar with writing simple documents in LaTeX. The MikTeX package is an excellent distribution of LaTeX for Windows and the WinShell environment is a good IDE for writing LaTeX documents. Both of these packages are available for free download and they are also installed on the College computers (at labs 217, 215).

Read more detailed information about the tools 

About the exercises and the final assignment

There will be 10 exercises, one almost every week, which you must prepare for the next week. If you won't prepare the exercises you won't be able to understand the subject of the course! 

The final grade for the course consists of 30% the exercises and 70% the assignment.