The Community for Technology Leaders
Green Image
<p><b>Abstract</b>—Amalia is a generator framework for constructing analyzers for operationally defined formal notations. These generated analyzers are components that are designed for customization and integration into a larger environment. The customizability and efficiency of Amalia analyzers owe to a computational structure called an inference graph. This paper describes this structure, how inference graphs enable Amalia to generate analyzers for operational specifications, and how we build in assurance. On another level, this paper illustrates how to balance the need for assurance, which typically implies a formal proof obligation, against other design concerns, whose solutions leverage design techniques that are not (yet) accompanied by mature proof methods. We require Amalia-generated designs to be transparent with respect to the formal semantic models upon which they are based. Inference graphs are complex structures that incorporate many design optimizations. While not formally verifiable, their fidelity with respect to a formal operational semantics can be discharged by inspection.</p>
Amalia, analysis software, engineering trade-offs, inference graphs, operational semantics, program transformations, proofs of correctness, transparent design.
Laura K. Dillon, R.E. Kurt Stirewalt, "Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components", IEEE Transactions on Software Engineering, vol. 29, no. , pp. 133-150, February 2003, doi:10.1109/TSE.2003.1178052
111 ms
(Ver 3.3 (11022016))