SE7103 FORMAL MODELS OF SOFTWARE SYSTEMS

SE7103       FORMAL MODELS OF SOFTWARE SYSTEMS

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   

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.