SE7103 FORMAL MODELS OF SOFTWARE SYSTEMS - ANNA UNIVERSITY 1ST SEM CSE SYLLABUS REG-2013 - Anna University Internal marks 2018
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:

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.