CSE 530 - 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. Previously CSE 537. Credit cannot be received for both CSE 530 and CSE 537.

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

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