CSE 530 Software Prototyping and Validation
(4 credits)
Description:
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.
Prerequisites: CSE 520 or CSE 537.