University of Minnesota
Master of Science in Software Engineering
/

You are here

SENG 5841: Formal Modeling and Analysis in Software Engineering

Traditionally, software development has been largely a manual endeavor. Validation that we are building the right system has been achieved through requirements and specification inspections and reviews. Verification that the system is developed to satisfy its specification is archived through inspections of design artifacts and extensive testing of the implementations.

In model-based development, the development effort is centered on a formal description of the proposed software system. For validation and verification purposes, this formal specification can then be subjected to various types of analysis, for example, completeness and consistency analysis, model checking, theorem proving, and test case generation. Through manual inspections, formal verification, and simulation and testing we convince ourselves (and any regulatory agencies) that the software specification possesses desired properties. The implementation is then automatically and correctly generated from this specification. There are currently several commercial and research tools that attempt to provide these capabilities—commercial tools are, for example, Esterel and SCADE from Esterel Technologies, Simulink and Stateflow from The Mathworks, Statemate from i-Logix, and SpecTRM from Safeware Engineering; and examples of research tool are SCR, and RSML-e.

In this course we will explore the concept of model-based development, its pros and cons, its impact on the development process, the formalisms and analysis techniques providing the foundation for the approach, and try our hand on commercial as well as research tools (tentatively, Simulink, Stateflow, TBD).

Course Goals

  • Understand the importance of modeling in software engineering.
  • Learn about different modeling and analysis approaches.
  • Try several approaches on examples and gain experience with some existing tools.
  • Learn how to critically read and evaluate research papers.
Course ID: 
SENG 5841
Complete Name of the Course: 
Formal Modeling and Analysis in Software Engineering
Intended Semester: 
elective