Formal methods (FM) introduction: What are FM? When, How and Why use FM? How project management can be done with FM: Gathering requirement, from Information Requirement to formal Specifications and validating formal specifications.
Introducing Z: What is Z? Informal requirements, data flow diagrams, state transition diagram, and state transition tables. Introducing schemas: Basic Bachelor of Engineering Program (2020) 43
types and abbreviations, axiomatic descriptions, state schemas, operation schemas, implicit preconditions and schema calculus
Elements of Z: Sets and types, declarations, variables, expressions, operators, predicates, equations and laws. Structure: Tuple, Records, Relations, Tables, Databases, Pairs and Binary Relations, Functions, Sequences and Operators.
Logic: Basic predicates, using predicates in Z, relations as predicates, logical connectives, logic and natural Language, quantifiers, Z and Boolean types, predicates and undefined expressions. Synthesis: Set comprehensives, lambda expressions, formal specifications, conveniences and shortcuts, modeling
systems and change
Schemas and schema calculus: Conjunctions and disjunctions, other schema operators. Schema types and bindings: Generics & free types.
Formal reasoning: Calculation and proof, laws, checking specifications, preconditions, formal reasoning and intuition, machine-checked proof.
Studies in Z: Document Control System, Text Processing, Eight Queens
Computer graphics and computational geometry. Rule-based programming:Essential elements, facts and rules, deducing new facts, checking the rules and specifying rule based programs
Graphical user interface: Events, display and dialogs, selecting a display, changing setting value, Z and state transition systems, changing the machine state.
Safety-critical protection system: Partition, refinement and enforcing the Safety Requirements.
Modeling large systems: A single subsystem, many subsystems, useful idioms, subsystems, conditions and modes.
Object-Oriented Programming model and Z, inherits and schema inclusion, OO Z dialects. Concurrency and Real-time
Refinement, program derivation and formal verification and converting Z specification into code.
Lectures (audio/video aids), Written Assignments/ Quizzes, Tutorials, Case Studies relevant to engineering disciplines, Semester Project, Guest Speaker, Industrial/ Field Visits, Group discussion, Report Writing
Mid Term, Report writing/ Presentation, Assignments, Project Report, Quizzes, Final Term
The Way of Z: Practical Programming with Formal Methods by Jonathan Jacky, Cambridge University Press.
Understanding Z: a Specification Language and its Formal Semantics. J. M. Spivey, Cambridge University Press, New York, NY, USA.
Modern Formal Methods and Applications, Hossam A. Gabbar, SpringerVerlag 200
There are 133 total credit hours to complete the Software Engineering degree.
