CP4002 Formal Models of Software Systems Syllabus:
CP4002 Formal Models of Software Systems Syllabus – Anna University PG Syllabus Regulation 2021
COURSE OBJECTIVES:
To understand the goals, complexity of software systems, the role of Specification activities and qualities to control complexity.
To understand the fundamentals of abstraction and formal systems
To learn fundamentals of logic reasoning- Propositional Logic, temporal logic and apply to models systems
To understand formal specification models based on set theory, calculus and algebra and apply to a case study
To learn Z, Object Z and B Specification languages with case studies.
UNIT I SPECIFICATION FUNDAMENTALS
Role of Specification- Software Complexity – Size, Structural, Environmental, Application, domain, Communication Complexity, How to Control Complexity. Software specification, Specification Activities-Integrating Formal Methods into the Software Lifecycle. Specification Qualities- Process Quality Attributes of Formal Specification Languages, Model of Process Quality, Product Quality and Utility, Conformance to Stated Goals Quality Dimensions and Quality Model.
UNIT II FORMAL METHODS
Abstraction- Fundamental Abstractions in Computing. Abstractions for Software Construction. Formalism Fundamentals – Formal Systems, Formalization Process in Software Engineering Components of a Formal System- Syntax, Semantics, and Inference Mechanism. Properties of Formal Systems – Consistency. Automata-Deterministic Finite Accepters, State Machine Modeling Nondeterministic Finite Accepters, Finite State Transducers Extended Finite State Machine. Case Study—Elevator Control. Classification of C Methods-Property-Oriented Specification Methods, Model-Based Specification Techniques.
UNIT III LOGIC
Propositional Logic – Reasoning Based on Adopting a Premise, Inference Based on Natural Deduction. Predicate Logic – Syntax and Semantics, Policy Language Specification, knowledge Representation Axiomatic Specification. Temporal Logic -. Temporal Logic for Specification and Verification, Temporal Abstraction Propositional Temporal Logic (PTL), First Order Temporal Logic (FOTL). Formal Verification, Verification of Simple FOTL, Model Checking, Program Graphs, Transition Systems.
UNIT IV SPECIFICATION MODELS
Mathematical Abstractions for Model-Based Specifications-Formal Specification Based on Set Theory, Relations and Functions. Property-Oriented Specifications- Algebraic Specification, Properties of Algebraic Specifications, Reasoning, Structured Specifications. Case Study—A Multiple Window Environment: requirements, Modeling Formal Specifications. Calculus of Communicating Systems: Specific Calculus for Concurrency. Operational Semantics of Agents, Simulation and Equivalence, Derivation Trees, Labeled Transition Systems.
UNIT V FORMAL LANGUAGES
The Z Notation, abstractions in Z, Representational Abstraction, Types, Relations and Functions, Sequences, Bags. Free Types-Schemas, Operational Abstraction -Operations Schema Decorators, Generic Functions, Proving Properties from Z specifications, Consistency of Operations. Additional Features in Z. Case Study: An Automated Billing System. The Object-Z Specification Language- Basic Structure of an Object-Z, Specification. Parameterized Class, Object-Orientation, composition of Operations-Parallel Communication Operator, Nondeterministic Choice Operator, and Environment Enrichment. The B-Method -Abstract Machine Notation (AMN), Structure of a B Specification, arrays, statements. Structured Specifications, Case Study- A Ticketing System in a Parking.
COURSE OUTCOMES:
CO1: Understand the complexity of software systems, the need for formal specifications activities and qualities to control complexity.
CO2: Gain knowledge on fundamentals of abstraction and formal systems
CO3: Learn the fundamentals of logic reasoning- Propositional Logic, temporal logic and apply to models systems
CO4: Develop formal specification models based on set theory, calculus and algebra and apply to a typical case study
CO5: Have working knowledge on Z, Object Z and B Specification languages with case studies.
TOTAL: 45 PERIODS
REFERENCES
1. Mathematical Logic for computer science ,second edition, M.Ben-Ari ,Springer,2012.
2. Logic in Computer Science- modeling and reasoning about systems, 2 nd Edition, Cambridge University Press, 2004.
3. Specification of Software Systems, V.S. Alagar, K. Periyasamy, David Grises and Fred B Schneider, Springer –Verlag London, 2011
4. The ways Z: Practical programming with formal methods, Jonathan Jacky, Cambridge University Press,1996.
5. Using Z-Specification Refinement and Proof,Jim Woodcock and Jim Devies Prentice Hall, 1996
6. Markus Roggenbach ,Antonio Cerone, Bernd-Holger Schlingloff, Gerardo Schneider , Siraj Ahmed Shaikh, Formal Methods for Software Engineering: Languages, Methods, Application Domains (Texts in Theoretical Computer Science. An EATCS Series) 1st ed. 2022 Edition