M.E. Software Engineering:Formal Methods
Master
In Patiala
Description
-
Type
Master
-
Location
Patiala
Facilities
Location
Start date
Start date
Reviews
Course programme
Semester I
Software Engineering Concepts and Methodologies
Software Design and Construction
Research Methodology
Software Architecture
Software Project Management
Semester II
Software Quality Management
Software Verification, Validation and Testing
Software Metrics
Advanced Topics in Software Engineering
Semester III
Seminar
Thesis (Starts)
Semester IV
Thesis (Continued)
Formal Methods
Introduction: aims of the module; assessment; teaching methods; style of presentation; harmful effects of deductivist style and Euclidean methodology.
Mathematical Modeling: how mathematics is used to model software components and systems.
Z's logical and mathematical toolkit: arithmetical relations and functions; propositional calculus, including useful laws; basic types (or given sets) and composite types, including set, Cartesian product and schema; typed predicate calculus; quantifiers, including restricted, unrestricted and unique; term-forming operators, including definite descriptions, conditional terms and local definitions; typed set theory; ways of making sets, including enumeration and comprehension; relations between sets and their members; operations on sets; some special sets; useful set-theoretic laws; relations, including heterogeneous and homogeneous; the calculus of relations, including domain, range, inverse, image, domain restriction and anti-restriction, range restriction and anti-restriction, composition, powers, identity, closures (including transitive and reflexive-transitive) and overriding; simple proofs; functions (including partial, total, injective, surjective and objective); sequences; and bags.
Specification and the schema calculus: state space; state schema; before and after schemas; state invariant; operation schemas; schema operations, including composition, piping, renaming, linking using propositional connectives, inclusion, hiding, the theta-operator, and pre-condition calculation; the Delta and Xi conventions; error schemas; partial and total specifications; several largish case-studies, including the internal telephone directory specification, a sales database, the bill of material problem, a route planner, Wing's library problem and a simple text-editor.
Refinement: abstract and concrete specifications; bridging the gap between them; proof-obligations and how they are discharged, including correspondence of initial states, correctness and applicability of operations; reification; decomposition; the retrieve relation, function and schema.
Verification: Hoare logic for a simple programming language including skip, assignment, sequencing, conditional, while-loop, repeat-loop, for-loop, procedures, functions, blocks and arrays; deriving a Hoare triple from a low-level Z specification; verification conditions; simple proofs; the philosophy of program verification; Fetzer and his critics; is certainty attainable?
Animation: the ideas behind functional programming languages and their suitability for animation; animating a Z specification in Haskell; why Haskell is better for this than both Miranda (tm) and ML; representing the basic types, the state space and the initial state; translating operations into Haskell; the role of the state invariant.
Other approaches: a look at the opposition, including Abrial's Abstract Machine Notation (AMN), B and VDM; why these are inferior to Z.
M.E. Software Engineering:Formal Methods