Oral Comprehensive Exam Details
Framework-based Construction of Formal Models
| Author: | Zebin Chen |
|---|---|
| Date: | February 03, 2005 |
| Time: | 12:00 |
| Location: | 220 Deschutes |
| Committee: | Stephen Fickas (Chair) Michal Young Stuart Faulk |
Abstract
Model checking is effective to discover subtle errors in concurrent programming. However, there is much resistance to its deployment in industrial applications. In addition to the fundamental problems, i.e. state space explosion and limited participants, the main obstacle is the expertise required in the formal modeling procedure. Such expertise includes logical abstraction, specification patterns, domain specific primitives, and search optimization algorithms that may or may not be sound or complete.
A framework is a well-established tool in software engineering, supporting design reuse as well as code reuse. We hypothesize that the framework concept can be applied to formal modeling as well, providing reuse of model designs and model code.
With the theme of framework-based formal modeling, we have conducted a survey of state-of-the-art model checkers and verifiers, including Spin, dSPIN, FSP, Alloy Analyzer, Bandera, MODEX, JPF2, Bogor, SCR and more. The public talk includes a discussion in selecting proper tools. It also includes a preliminary case study we have built around a specific application area (ubiquitous computing) and a specific formal modeling language (Promela). We show that frameworks have the potential to ease formal modeling by reusing expertise, and hypothesize that framework-based light-weight formal modeling is a promising way to promote the deployment of model checkers. Problems and future directions are discussed in the talk.