**CP5006 FORMAL MODELS OF SOFTWARE SYSTEMS SYLLABUS**

**REGULATION 2017**

**ME CSE - SEMESTER 3**

**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 Life-Cycle. 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.

**TOTAL :45 PERIODS**

OUTCOMES:

OUTCOMES:

Upon completion of this course, the students should be able to

- Understand the complexity of software systems, the need for formal specifications activities and qualities to control complexity.
- Gain knowledge on fundamentals of abstraction and formal systems
- Learn the fundamentals of logic reasoning- Propositional Logic, temporal logic and apply to models systems
- Develop formal specification models based on set theory, calculus and algebra and apply to a typical case study
- Have working knowledge on Z, Object Z and B Specification languages with case studies.

**REFERENCES:**

- Mathematical Logic for computer science ,second edition, M.Ben-Ari ,Springer,2003.
- Logic in Computer Science- modeling and reasoning about systems, 2 nd Edition, Cambridge University Press, 2004.
- Specification of Software Systems, V.S. Alagar, K. Periyasamy, David Grises and Fred B Schneider, Springer –Verlag London, 2011
- The ways Z: Practical programming with formal methods, Jonathan Jacky, Cambridge University Press,1996.
- Using Z-Specification Refinement and Proof,Jim Woodcock and Jim Devies Prentice Hall, 1996
- Z: An introduction to formal methods, Second Edition, Antoi Diller, Wiley, 1994.

Awesome blog. Very useful information, it clarified a lot of things to us. Thanks for sharing your view.- dentist in district heights md

ReplyDeleteHealthy Dental

https://healthydental.com/