Recent years have witnessed a steady increase in the use of software
modeling techniques in industry. There is a growing appreciation
for the fact that developing and reasoning about models of software
systems can help to improve the quality of software implementations.
This is undoubtedly a positive trend, but much work remains to capitalize
on the potential benefits of the pervasive use of modeling and automated
model analysis in software development.|
In this talk, I will present ongoing research at the University of Nebraska and Kansas State University that adopts a broad view of what constitutes software (e.g., requirements specifications, architectural and design models, and implementations) and of what constitutes analysis (e.g., lightweight structural analyses, flow analyses for bug finding, and model checking). A central theme of our work is the customization of analyses to a software modeling "domain" (i.e., a family of models that capture a specific level of abstraction of a specific class of systems). By customizing analyses, we can target them to important properties of the selected domain, optimize their performance to exploit the semantics of domain primitives, and present analysis results in terms of those primitives to improve user understanding.
To illustrate the benefits of customization, I will present our work on designing, building, and applying Bogor -- highly-configurable framework for implementing domain-specific software model checkers. Bogor has been applied to implement analyses for a wide range of software models including: design models of real-time embedded systems, UML state machines, multi-threaded Java programs, and MPI-based high-performance computing architectures; I will describe several of these applications in detail. Bogor is distributed freely for educational and research use and has been adopted by a large number of institutions. This is due, in part, to an extensive set of course and tutorial materials for teaching model checking based on Bogor that we have developed and that I will describe.
|This talk will give an introduction to Martin-Lof's constructive type theory. This constructive type theory was originally developed around 1970 as a formal system which provides a foundation for constructive mathematics. It is also a programming language with a very expressive type system. The types can express virtually any possible property of a program and can therefore be used as a specification language. Martin-Lof type theory and related systems have also been the basis for several proof assistants (interactive theorem provers) such as the Coq system (based on the Calculus of Constructions), the NuPRL system (based on extensional Martin-Lof type theory) and the Agda system (based on intensional type theory). I will discuss some of the design decisions behind the Agda system.|