CP5006 FORMAL MODELS OF SOFTWARE SYSTEMS SYLLABUS - ANNA UNIVERSITY PG REGULATION 2017 - Anna University Internal marks 2018

CP5006 FORMAL MODELS OF SOFTWARE SYSTEMS SYLLABUS - ANNA UNIVERSITY PG REGULATION 2017

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:

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:
  1. Mathematical Logic for computer science ,second edition, M.Ben-Ari ,Springer,2003.
  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. Z: An introduction to formal methods, Second Edition, Antoi Diller, Wiley, 1994.

1 comment:

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

    Healthy Dental
    https://healthydental.com/

    ReplyDelete