Sound Methods and Effective Tools for Engineering Modeling and Analysis

Abstract

Modeling and analysis is indispensable in engineering. To be both safe and effective, a modeling method requires a modeling language with a validated semantics; feature-rich, easy-to-use, dependable tools; and low engineering costs. Today we lack cost-effective means to develop such methods. One goal of our long-terms research program is to develop such capabilities. In this talk we present a partial solution combining several ideas: formal methods for language design; package-oriented programming to provide rich function and usability; and testing based on a form of bounded model checking. We are evaluating the approach with particular attention to technical- and cost- effectiveness in an end-to-end experiment. We first deployed an existing method for probabilistic risk assessment to NASA in a package-oriented tool and surveyed engineers to assess its usability. We then formally specified, improved, and validated the PRA modeling language. To assess cost, we built a package-based tool for the new language. In as yet unpublished work, we are evaluating a testing strategy using a bounded model checking technique (Marinov, Khurshid, Jackson). Our data suggest that the approach can enable cost- effective deployment and use of sound methods of modeling and analysis. This is joint with David Coppit, College of William and Mary: D. Coppit and Sullivan, K.J., "Sound Methods and Effective Tools for Engineering Modeling and Analysis," to appear, Proceedings of the 25th International Conference on Software Engineering, Portland, OR, 2003.