CSI5300

Software Prototyping and Validation

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, CSE 530. Credit can be received for only one of CSE 530, CSI 5300, or CSE 537.

CSE530, CSE537

School of Egr. and Comp. Sci.