**ANNA UNIVERSITY, CHENNAI**

**REGULATIONS - 2013**

**M.E. COMPUTER SCIENCE AND ENGINEERING**

**SE7103 FORMAL MODELS OF SOFTWARE SYSTEMS**

**OBJECTIVES:**

To understand the basic elements of Z

To understand relations, functions, and logical structures in Z

To understand Z schemas and schema calculus

To learn selected Z case studies

To understand Z schema refinement

**UNIT I FOUNDATIONS OF Z**

Understanding formal methods – motivation for formal methods – informal requirements to formal specifications – validating formal specifications – Overview of Z specification – basic elements of Z – sets and types – declarations – variables – expressions – operators – predicates and equations

**UNIT II STRUCTURES IN Z**

Tuples and records – relations, tables, databases – pairs and binary relations – functions – sequences – propositional logic in Z – predicate logic in Z – Z and boolean types – set comprehension – lambda calculus in Z – simple formal specifications – modeling systems and change

**UNIT III Z SCHEMAS AND SCHEMA CALCULUS**

Z schemas – schema calculus – schema conjunction and disjunction – other schema calculus

operators – schema types and bindings – generic definitions – free types – formal reasoning –

checking specifications – precondition calculation – machine-checked proofs

**UNIT IV Z CASE STUDIES**

Case Study: Text processing system – Case Study: Eight Queens – Case Study: Graphical User Interface – Case Study: Safety critical protection system – Case Study: Concurrency and real time systems

**UNIT V Z REFINEMENT**

Refinement of Z specification – generalizing refinements – refinement strategies – program

derivation and verification – refinement calculus – data structures – state schemas – functions and relations – operation schemas – schema expressions – refinement case study

**TOTAL : 45 PERIODS**

OUTCOMES:

OUTCOMES:

Upon Completion of the course,the students will be able to

Apply the basic elements of Z

Develop relational, functional, and logical Z structures

Develop Z schema as models of software systems

Perform verifications and conduct proofs using Z models

Refine Z models towards implementing software systems

**REFERENCES:**

1. Jonathan Jacky, “The way of Z: Practical programming with formal methods”, Cambridge

University Press, 1996.

2. Antoni Diller, “Z: An introduction to formal methods”, Second Edition, Wiley, 1994.

3. Jim Woodcock and Jim Davies, “Using Z – Specification, Refinement, and Proof”, Prentice

Hall, 1996.

4. J. M. Spivey, “The Z notation: A reference manual”, Second Edition, Prentice Hall, 1992.

5. M. Ben-Ari, “Mathematical logic for computer science”, Second Edition, Springer, 2003.

6. M. Huth and M. Ryan, “Logic in Computer Science – Modeling and Reasoning about

systems”, Second Edition, Cambridge University Press, 2004.

## No comments:

## Post a Comment