
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 133150, February, 2003.  
BibTex  x  
@article{ 10.1109/TSE.2003.1178052, author = {Laura K. Dillon and R.E. Kurt Stirewalt}, title = {Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components}, journal ={IEEE Transactions on Software Engineering}, volume = {29}, number = {2}, issn = {00985589}, year = {2003}, pages = {133150}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2003.1178052}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components IS  2 SN  00985589 SP133 EP150 EPD  133150 A1  Laura K. Dillon, A1  R.E. Kurt Stirewalt, PY  2003 KW  Amalia KW  analysis software KW  engineering tradeoffs KW  inference graphs KW  operational semantics KW  program transformations KW  proofs of correctness KW  transparent design. VL  29 JA  IEEE Transactions on Software Engineering ER   
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 Amaliagenerated 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 ComponentBased Approach to Building Formal Analysis Tools,” Proc. 2001 Int'l Conf. Software Eng. (ICSE '01), pp. 167176, 2001.
[2] D. Parnas, “Designing Software for Ease of Extension and Contraction,” IEEE Trans. Software Eng., vol. 5, no. 2, pp. 128138, 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 ObjectOriented Software, AddisonWesley, Reading, Mass., 1994.
[5] D. Batory and S. O'Malley, "The Design and Implementation of Hierarchical Software Systems with Reusable Components," ACM TOSEM, pp. 355398, 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. 6573.
[8] G.D. Plotkin, “A Structural Approach to Operational Semantics,” Technical Report DAIMI FN19, 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. 2373, 1989.
[10] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. SpringerVerlag, 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 CollaborationBased Design,” Technical Report MSUCSE016, 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, ”ObjectOriented 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, “AspectOriented Programming,” European Conf. ObjectOriented Programming (ECOOP '97), M. Aksit and S. Matsuoka, eds., pp. 220242, 1997.
[16] K. Fisler and S. Krishnamurthi, “Modular Verification of CollaborationBased Software Designs,” Proc. ESEC/ACM SIGSOFT Conf. Foundations of Software Eng., V. Gruhn, ed., pp. 152163, Sept. 2001.
[17] X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, K. Birman, and R. Constable, “Bulding Reliable, HighPerformance Communication Systems from Components,” Operating Systems Rev., vol. 34, no. 5, pp. 8092, Dec. 1999.
[18] Y. Smaragdakis and D. Batory, “Implementing Layered Designs with Mixin Layers,” Proc. 12th European Conf. ObjectOriented 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. 1424.
[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. 304318, Apr. 1992.
[21] R. Cleaveland and S. Sims, “Generic Tools for Verifying Concurrent Systems,” Science of Computer Programming, vol. 42, no. 1, pp. 3947, 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 StateSpace Analysis Tools,” Proc. 19th IEEE Int'l Conf. Software Eng., W.R. Adrion, ed., pp. 239250, 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. 1116, July 1998.
[26] A.J. Camilleri, “Mechanizing CSP Trace Theory in Higher Order Logic,” IEEE Trans. Software Eng., vol. 16, no. 9, pp. 9931004, 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. 3949, 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. 341358, 1999.
[29] J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. AddisonWesley, 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. 120129, 2000.
[31] L.K. Dillon, G. Kutty, L.E. Moser, P.M. MelliarSmith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. Methods, vol. 3, no. 2, pp. 131165, 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. 7989, 2000.