23rd International Conference on Software Engineering (ICSE'01)
Lightweight Analysis of Operational Specifications Using Inference Graphs
Toronto, Canada
May 12-May 19
ISBN: 0-7695-1050-7
Abstract: The Amalia framework generates lightweight components that automate the analysis of operational specifications and designs [16]. 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. It creates and evaluates an inference graph on-the-fly during a top-down traversal of a specification to deduce the specification's local behaviors (called steps). 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. Inference graphs are a clean abstraction that can be formally defined. The paper provides a detailed, but informal, introduction to inference graphs. It uses example specifications written in LOTOS for purposes of illustration.
Index Terms:
Testing, analysis, and verification; Patterns and frameworks; Formal methods; Lightweight analysis components; Operational specifications; Automated software generators.
Citation:
Laura K. Dillon, R. E. Kurt Stirewalt, "Lightweight Analysis of Operational Specifications Using Inference Graphs," icse, pp.0057, 23rd International Conference on Software Engineering (ICSE'01), 2001