This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components
February 2003 (vol. 29 no. 2)
pp. 133-150

Abstract—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.

[1] R.E.K. Stirewalt and L.K. Dillon, “A Component-Based Approach to Building Formal Analysis Tools,” Proc. 2001 Int'l Conf. Software Eng. (ICSE '01), pp. 167-176, 2001.
[2] D. Parnas, “Designing Software for Ease of Extension and Contraction,” IEEE Trans. Software Eng., vol. 5, no. 2, pp. 128-138, 1979.
[3] L.K. Dillon and R.E.K. Stirewalt, “Lightweight Analysis of Operational Specifications Using Inference Graphs,” Proc. 2001 Int'l Conf. Software Eng. (ICSE '01), pp. 57–67, 2001.
[4] E. Gamma et al., Design Patterns: Elements of Object-Oriented Software, Addison-Wesley, Reading, Mass., 1994.
[5] D. Batory and S. O'Malley, "The Design and Implementation of Hierarchical Software Systems with Reusable Components," ACM TOSEM, pp. 355-398, Oct. 1992.
[6] B. Stroustrup, The Design and Evolution of C++. Addison Wesley, 1994.
[7] J.M. Boyle, R.D. Resler, and V.L. Winter, "Do You Trust Your Compiler?" Computer, May 1999, pp. 65-73.
[8] G.D. Plotkin, “A Structural Approach to Operational Semantics,” Technical Report DAIMI FN-19, Computer Science Dept., Aarhus Univ., 1981, http://www.dcs.ed.ac.uk/home/gdp/publications SOS.ps.gz.
[9] T. Bolognesi and E. Brinksma, “Introduction to the ISO Specification Language Lotos,” The Formal Description Technique Lotos, P.H.J. van Eijk, C.A. Vissers, and M. Diaz, eds., pp. 23-73, 1989.
[10] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
[11] I. Attali and D. Parigot, “Integrating Natural Semantics and Attribute Grammars: The Minotaur System,” Technical Report 2339, INRIA Sophia Antipolis, 1994.
[12] L.K. Dillon and R.E.K. Stirewalt, “An Example Proof of Correctness for a Collaboration-Based Design,” Technical Report MSU-CSE-01-6, Computer Science and Eng. Dept., Michigan State Univ., East Lansing, Mar. 2001, www.cse.msu.edu/~ldillon/Sel_pubsig.ps.
[13] A.W. Appel, Compiling with Continuations. Cambridge Univ. Press, 1992.
[14] K.J. Lieberherr and C. Xiao, ”Object-Oriented Software Evolution,” IEEE Trans. Software Eng., vol. 19, no. 4, pp. 313–343, Apr. 1993.
[15] G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, , C. Lopes, J.-M. Loingtier, and J. Irwin, “Aspect-Oriented Programming,” European Conf. Object-Oriented Programming (ECOOP '97), M. Aksit and S. Matsuoka, eds., pp. 220-242, 1997.
[16] K. Fisler and S. Krishnamurthi, “Modular Verification of Collaboration-Based Software Designs,” Proc. ESEC/ACM SIGSOFT Conf. Foundations of Software Eng., V. Gruhn, ed., pp. 152-163, Sept. 2001.
[17] X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, K. Birman, and R. Constable, “Bulding Reliable, High-Performance Communication Systems from Components,” Operating Systems Rev., vol. 34, no. 5, pp. 80-92, Dec. 1999.
[18] Y. Smaragdakis and D. Batory, “Implementing Layered Designs with Mixin Layers,” Proc. 12th European Conf. Object-Oriented Programming, 1998.
[19] P. Borras et al., "Centaur: The System," Proc. Third Symp. Software Development Environments (ACM SIGSOFT '88), ACM Press, New York, 1988, pp. 14-24.
[20] G.A. Venkatesh and C.N. Fischer, “Spare: A Development Environment for Program Analysis Algorithms,” IEEE Trans. Software Eng., vol. 18, no. 4, pp. 304-318, Apr. 1992.
[21] R. Cleaveland and S. Sims, “Generic Tools for Verifying Concurrent Systems,” Science of Computer Programming, vol. 42, no. 1, pp. 39-47, 2002.
[22] H. Garavel, “OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing,” Proc. First Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), 1998.
[23] M. Pezzè and M. Young, “Constructing Multiformalism State-Space Analysis Tools,” Proc. 19th IEEE Int'l Conf. Software Eng., W.R. Adrion, ed., pp. 239-250, May 1997.
[24] Reasoning Systems Incorporated, Palo Alto, Calif., Refine User's Guide, 2002.
[25] B. Gramlich and F. Pfenning, “Strategic Principles in the Design of Isabelle,” Proc. Workshop Strategies in Automated Deduction, pp. 11-16, July 1998.
[26] A.J. Camilleri, “Mechanizing CSP Trace Theory in Higher Order Logic,” IEEE Trans. Software Eng., vol. 16, no. 9, pp. 993-1004, Sept. 1990.
[27] N.A. Day and J.J. Joyce, “A Framework for Multinotation Specification and Analysis,” Proc. Fourth IEEE Int'l Conf. Requirements Eng. (ICRE 2000), pp. 39-49, June 2000.
[28] N.A. Day and J.J. Joyce, “Symbolic Functional Evaluation,” Proc. 12th Int'l Conf., Theorem Proving in Higher Order Logics (TPHOLs), pp. 341-358, 1999.
[29] J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Apr. 1979.
[30] G. Luttgen, M. vonderBeeck, and R. Cleaveland, “A Compositional Approach to Statecharts Semantics,” Proc. ACM SIGSOFT Symp. Foundations of Software Eng. (FSE 2000), D. Rosenblum, ed., pp. 120-129, 2000.
[31] L.K. Dillon, G. Kutty, L.E. Moser, P.M. Melliar-Smith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. Methods, vol. 3, no. 2, pp. 131-165, Apr. 1994.
[32] J.S. Robbins and D.F. Redmiles, “Cognitive Support, UML Adherence, and XMI Interchange in ArgoUML,” Information and Software Technology, vol. 42, no. 2, pp. 79-89, 2000.

Index Terms:
Amalia, analysis software, engineering trade-offs, inference graphs, operational semantics, program transformations, proofs of correctness, transparent design.
Citation:
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. 2, pp. 133-150, Feb. 2003, doi:10.1109/TSE.2003.1178052
Usage of this product signifies your acceptance of the Terms of Use.