Courses Developed and Taught by Prof. Janusz Laski  
STAD, OU - Prof. J. Laski & P. Luczycki
Procomp, OU - Prof. J. Laski & W. Szermer & W.F. Stanley
 
Swat, Softools Inc.,
 
Short Introduction to VDM-Tools
 
Short Introduction to Spark Systems
 
back to courses

     

CSE 437/537


SYSTEMATIC

 		     
  

 SOFTWARE 

 		  
     

 DEVELOPMENT 


To download zipped Stages 1 - 3.zip document click here.

To Open/Cut/Paste Stages 1 - 3.vdm document click here.
From the menu select Edit/Select All then Edit/Copy. After completing those steps,
open Notepad. From the Notepad's menu select Edit/Past. This will copy
content's of "stages1-3.vdm" document from the WEB to notepad. Save the document
to your hard drive or other place with the file type extention "*.vdm". You now can
start using "stages1-3.vdm" with the VDM-SL Toolbox.

INSTRUCTOR:  Professor Janusz Laski

The course is an introduction to a systematic software development
paradigm, using mathematical specification techniques to model the
software artifacts at various stages of its development in a precise,
unambiguous way. Towards that goal, the Vienna Development Method
Specification Language (VDM-SL) is used. It is an internationally
standardized specification language, supported by IFAD Toolbox. The most
recent version of the Toolbox has been installed in the Software Testing
and Verification Laboratory (room 101 SEB) and is also available in a
dial up version. However, the textbook comes with a CD-ROM, which contains
a restricted version of the Toolbox, Toolbox Lite, which is usually
sufficient for the first half of the course.

The course is centered around a nontrivial, language-independent
term project. The project starts with the specification of
the problem and proceeds towards operational and data abstraction refinement;
coding in the language of your choice is the last stage of the project.
Formal techniques are introduced gradually, in step with the project, as
needs arise rather than as a goal in and of itself. An emphasis is placed
on practical potential and limitations of the method. Thus, in an ideal
scenario the final product should be bug-free; in practice, it is almost the
case but the amount of testing is significantly reduced.

TEXT: John Fitzgerald, Peter Gorm Larsen, “Modeling Systems:
Practical Tools and Techniques in Software Development,”
Cambridge University Press, 1998. This is a rather undergraduate
text but it is the only one that offers a fairly readable introduction
to the VDM-SL language and the Toolbox.

REFERENCES:

  1. C.B.Jones, Systematic Software Development Using VDM, Prentice-Hall, 1990
  2. J.Woodcock, M.Loomes, "Software Engineering Mathematics," Addison-Wesley,
  3. Andrew Harry, Formal methods: Fact File, VDM and Z, John Wiley&Sons, 1996


TOPICS (tentative).

  • Program development cycle
  • Specifications of functions and operations
  • Basic abstract types
    • sets
    • sequences
    • mappings
    • relations
  • Operation refinement
    • proof obligations for structured constructs
    • inductive assertions
    • step-wise correctness preserving refinement
  • Data refinement
    • Abstract Data Types (ADT, aka User Defined Types) in program development
    • Representation of ADT
    • Proof Obligations
PREREQUISITES:
  • Fluency in programming and a good command of data structures
  • APM 563 and CSE 510 a great plus.


To see the structure of a term project, see CSE437/537.Project.