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 require such a translation. 

  The Amalia framework generates lightweight components that automate
  the analysis of operational specifications and designs.  A key
  concept is the step analyzer, which enables Amalia to automatically
  tailor high-level analyses, such as behavior simulation and model
  checking, to different specification languages and representations.
  A step analyzer uses a new abstraction, called an inference graph,
  for the analysis.  The nodes of an inference graph directly reify
  the rules in an operational semantics, enabling Amalia to
  automatically generate a step analyzer from an operational
  description of a notation's semantics. 

  This talk will provide an overview of the approach to producing
  lightweight tools used in Amalia.  It will describe inference graphs
  and provide an example using Lotos.