Name
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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1109/ICSE.2001.919081 | ICSE |
Keywords | DocType | ISSN |
application generators,computer aided software engineering,formal specification,formal verification,graphs,inference mechanisms,subroutines,Amalia framework,LOTOS,automated software generator,behavior simulation,design patterns,formal methods,formal verification,formally defined abstraction,high-level analyses,inference graphs,lightweight components,lightweight specification analysis,model checking,notation semantics,operational description,operational semantics,operational specifications,representations,software testing,specification languages,specification local behavior,step analyzer,top-down specification traversal | Conference | 0270-5257 |
ISBN | Citations | PageRank |
0-7695-1050-7 | 4 | 0.44 |
References | Authors | |
9 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Laura K. Dillon | 1 | 497 | 70.70 |
| R. E. Kurt Stirewalt | 2 | 51 | 4.03 |