CS&E Colloquium: Requirements, models, properties, and analysis: How do they all fit together?
The computer science colloquium takes place on Mondays from 11:15 a.m. - 12:15 p.m.
This week's speaker, University of Minnesota's Department of Computer Science Chair and Professor, Mats Heimdahl, will be giving a talk titled "Requirements, models, properties, and analysis: How do they all fit together?"
Getting the system requirements right in a development project is crucial for success. One highly promising approach to rigorous requirements capture and definition is modeling of the requirements in formal notations. In such Model-Based Requirements Engineering, an initial set of natural language requirements forms the basis for an initial behavioral model of the intended system behavior as well as the basis for an initial formalization of the natural language requirements into formal requirements properties. Formal verification now allow formal verification techniques to be used to analyze the set of requirements properties as well as the behavioral models. For example, the set of requirements properties can be checked for consistency and the behavioral model can be verified against the formalized requirements properties. The
results from this analysis can then be used in an iterative requirements validation process where the analysis results serve as a basis for the modification, refinement, and extension of the set of requirements and/or the behavioral models to bring them in conformance with the truly desired (or notional) system requirements.
Over 20 years of research (and many case studies and development efforts), we have accumulated a wealth of experiences in model-based development and requirements engineering that provide the foundation for the research covered in this talk. The goal of the presentation is threefold. First, we aim to clarify the often confused relationships between natural language requirements, formal behavioral models, and formally captured requirements. Second, we will describe how one can use verification techniques to ensure that (1) the model indeed behaves as stated in the requirements,(2) that the requirements are the “true” requirements needed to meet the system objectives, and (3) that the analysis results can be used to better understand the characteristics of the system being developed. Finally, we want to spend some time opportunities for future research.
Mats Heimdahl is the Department Head and a Professor of Computer Science & Engineering at the University of Minnesota. He earned an M.S. in Computer Science and Engineering from the Royal Institute of Technology (KTH) in Stockholm, Sweden and a Ph.D. in Information and Computer Science from the University of California at Irvine.
His research interests are in software engineering, safety critical systems, software safety, testing, requirements engineering, formal specification languages, and automated analysis of specifications.