A Component-Based Approach to Building Formal Analysis Tools

DOI 10.1109/icse.2001.919091 dblp

Abstract

Automatic-verification capability tends to be packaged into stand-alone tools, as opposed to components that are easily integrated into a larger software-development environment. Such packaging complicates integration because it involves translating internal representations into a form compatible with the stand-alone tool. By contrast, lightweight-analysis components package analysis capability in a form that does not involve such a translation. Borrowing ideas from GenVoca and object-oriented design patterns, we developed a domain model and an automatic generation framework for lightweight-analysis components. The generated components operate directly over the internal form of a specification without requiring a change in representation. Moreover, the domain model identifies several "useful subsets" that can be used to customize analysis capability to a particular application. We validated this domain model by generating lightweight analyzers for temporal logic and the behavioral subset of Lotos.

BibTeX

@inproceedings{Stirewalt-Dillon:ICSE01,
  author    = {Kurt Stirewalt and
               Laura K. Dillon},
  title     = {A {Component-Based} Approach to Building Formal Analysis Tools},
  booktitle = {ICSE},
  pages     = {167--176},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

A Component-Based Approach to Building Formal Analysis Tools

Abstract

Related papers