CSE 5300 - Software Prototyping and Validation

(4 credits)

This is a project-oriented course geared towards the creation of a validated, interpretable and thoroughly tested model of software for which, in most cases, C++ code can be automatically generated. It builds on the VDM-SL notation covered in CSE 520 and is supported by the VDM-SL Toolbox, TOPICS: Program development cycle. Principles of step-wise, correctness preserving refinement. Requirements synthesis; Direct and indirect models; Operation refinement for structured programming constructs. Data refinement: Abstract Data Types (ADT) in program development, user-defined types, representation of ADT. Model validation: testing and proof obligations; automated random testing of the final model using an executable postcondition of the problem as a test oracle. Credit can be received for only one of CSE 5300, or CSE 537.

Prerequisite(s): Student must meet prerequisite (CSE 5200 or CSE 537).

Course revisions made after the Graduate Catalog publication date will be posted in the Graduate Catalog Addendum.