SE7103 FORMAL MODELS OF SOFTWARE SYSTEMS - ANNA UNIVERSITY 1ST SEM CSE SYLLABUS REG-2013

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.

URL: http://feedproxy.google.com/~r/StudentsBlog100/~3/-G104l2AZPA/se7103-formal-models-of-software-systems-anna-univ-pg-csr-reg-2013-syllabus.html