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 510


Fundamentals

 of Software

 		  
  

 Engineering

 Modelling



Instructor:  Janusz Laski

This course introduces the students to the

    Fundamentals of Software Engineering Modelling
and is based upon the following two tenets:

  1. “Computer Science is Mathematics at Work,” corresponding
    to the generally accepted notion that “Engineering is
    Science at Work", and

  2. ”Whenever possible, the math involved should be supported
    by software tools.”

    These assumptions lead to the following consequences. First,
    the mathematical topics covered are those needed in the analysis
    and modeling of problems emerging in computer science and software
    engineering, hence they do not necessarily fall into the category
    of typical discrete mathematics. Second, the applications of the
    mathematics to software development, rather than its inherent
    theoretical properties, are emphasized. Third, whenever possible,
    software supporting tools are used to give the students the feeling
    of the mathematics as a real engineering tool serving essential
    and irreplaceable modeling functions.

Most of the course consists of lectures by the instructor
and discussions of the assignments.
There are two exams (midterm and final) and five to six
assignments during the course, perhaps split into several parts.
Most assignments involve experiments with relevant software tools,
to name only two:

  1. IFAD Toolbox, that supports the Vienna Development Method (VDM),
    a set-based software specification language and

  2. SPARK, a Safety Critical subset of Ada, an integrated
    software analysis tool, whose interactive Proof Checker supports
    proving theorems germane to computer science. If the class is small,
    a presentation to the class can be required in lieu of one assignment.
Prerequisite: CSE 504 or equivalent.

Text: There is no single text that covers all topics in the course.
However, the selected book,

    “Introductory Logic and Sets for Computer Scientists,”
    Addison-Wesley, 1999,
by Nimal Nissanke, offers the best approximation.
Its main advantage is great clarity and a sound connection to the real
world. However, this is essentially an undergraduate text and it will
be supplemented by additional material to be distributed in class.

References.
J.Woodcock, M.Loomes, “Software Engineering Mathematics,” Addison-Wesley, 1988.

The Lab. The EDS-supported Software Verification and Testing Laboratory is located
in 101 SEB. It has eight NT-based seats and also supports a dial-in services for
some tools. Instructions about its use will be distributed in class.


Topics (tentative, might change depending on class size and progress made):
  • Propositions
  • Predicate calculus
  • Sets and set operations
  • Relations
  • Graphs
  • Functions
  • Sequences and bags
  • Maps
  • Lambda abstraction of functions
    (the above topics involve experiments with IFAD Toolbox).
  • Transformation Proofs
  • Deductive Proofs
  • Inference Rules and Proof Strategies
    (that part of the course involves experiments with SPADE Simplifier and interactive
    Proof Checker).


To see a sample of typical assignments, see CSE510.ASSIGNMENTS.