SE7103 FORMAL MODELS OF SOFTWARE SYSTEMS Syllabus
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
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.
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
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.