Abstract
Large systems are invariably built from assembled components. It is essential for such systems to have predictable behavior, if the risks of failure are too high. To enable practical and modular verification of industrial-strength systems, software practitioners need to learn to build both behavioral specifications of components and component implementations that are annotated with suitable internal assertions. Neither of these tasks can be automated, in general. However, once suitable specifications and implementations of components are given, a mechanical system (with human assistance) can check in a modular and scalable fashion if component-based software behaves as specified. To illustrate the issues, the paper presents a non-trivial component-based example. The example underscores that predictable component-based construction is challenging, and that it cannot become practical, without educating students and software developers on principles of mathematical specifications and correct, efficient implementations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ernst, G. W., Hookway, R. J., Menegay, J. A., and Ogden, W. F., “Modular Verification of Ada Generics,” Computer Languages, Vol.16, No. 3/4, 1991, pp. 259–280.
Fetzer, J. H., “Program Verification: The Very Idea”, Communications of the ACM, Vol.31, No.9, Sep 1988, pp. 1048–1063
Fleming, D. Foundations of Object-Based Specification Design. Ph.D. Dissertation, Dept. of Computer Science and Electrical Engineering, West Virginia Univ., Morgantown, WV, 1997.
Fleming, D., Sitaraman, M., and Sreerama, S., “A Performance Criterion for Object Interface Design,” J. Object-Oriented Programming, Jul/Aug. 1997, pp. 52–63.
Garlan, D. and Perry, D., “Introduction to the Special Issue on Software Architecture,” IEEE Trans. Software Engineering, Apr. 1995.
Guttag, J. V. and Horning, J. J., Larch: Languages and Tools for Formal Specification, Springer-Verlag, 1992.
Harms, D.E., and Weide, B.W., “Copying and Swapping: Influences on the Design of Reusable Software Components,” IEEE Trans. Software Engineering, Vol. 17, No. 5, May 1991, pp. 424–435.
J. Hollingsworth, S. Sreerama, B.W. Weide, and S. Zhupanov, “RESOLVE Components in Ada and C++,” ACM SIGSOFT Software Engineering Notes, Vol. 19, No. 4, Oct. 1994, pp. 52–63.
Jones, C. B., Systematic Software Development Using VDM, Prentice-Hall, Englewood Cliffs, NJ, 1990.
Kozaczynski, V. and Ning, J. Q., “Panel discussion on Component-Based Software Engineering,” Proc. 4th Int’l Conf. Software Reuse, IEEE CS Press, 1996, 236–242.
W. Leal and A. Arora, A foundation for component verification in RESOLVE, Technical Report OSU-CISRC-4/99-TR11.
Leavens, G., “Modular Specification and Verification of Object-Oriented Programs,” IEEE Software, Vol. 8, No. 4, Jul. 1991, pp. 72–80.
Leavens, G. T., and Nierstrascz, O., Sitaraman, M., “1997 Workshop on Foundations of Component-Based Systems,” ACM SIGSOFT Software Engineering Notes, Vol. 23, No. 1, Jan. 1998, pp. 38–41.
Long, T. J., Weide, B. W., Bucci, P., Gibson, D. S., Hollingsworth, J. E., Sitaraman, M., and Edwards, S., “Providing Intellectual Focus to CS1/CS2,” Proc. 29th SIGCSE Symp. Computer Science Education, ACM Press, pp. 252–256.
Long, T. J., Weide, B. W., Bucci, P., and Sitaraman, M., “Client View First: An Exodus from Implementation-Biased Teaching,” Proc. 30th SIGCSE Symp. Computer Science Education, ACM Press, 1999, pp. 136–140.
Luckham, D., Programming with Specifications, Springer-Verlag, 1990.
Meyer, B., “On Formalism in Specifications,” IEEE Software, Vol. 2, No. 1, Jan. 1985, pp. 6–26.
Meyer, B., Object-Oriented Software Construction, 2nd Edition, Prentice Hall PTR, Upper Saddle River, New Jersey, 1997.
Musser, D. R. and Saini, A., STL Tutorial and Reference Guide, Addison-Wesley, Reading, MA, 1996.
Proc. NASA Focus on Software Reuse Workshop, Fairfax, Virginia, Sept. 1996.
Odgen, W.F., The Proper Conceptualization of Data Structures, Class Notes, Dept. of Computer and Info. Sciences, The Ohio State Univ., 1997.
Owre, S., Rushby, J., Shankar, N., von Henke, F. “Formal Verification of Fault-Tolerant Architectures: Prolegomena to the Design of PVS.” IEEE Trans. Software Engineering, Vol. 21, No. 2, Feb. 1995, pp. 107–125.
Sitaraman, M., Harms, D.E., and Welch, L.W., “On Specification of Reusable Software Components,” Int’l J. Software Engineering and Knowledge Engineering, Vol. 3, No. 2, June 1993, pp. 207–229.
Sitaraman, M., and Weide, B.W., eds. “Com-po-nent-Based Software Engineering Using RESOLVE,” ACM SIGSOFT Soft-ware Engineering Notes, Vol. 19, No. 4, 1994, pp. 21–67.
Sitaraman, M., “Impact of Performance Considerations on Formal Specification Design,” Formal Aspects of Computing, Springer-Verlag Int’l, Vol. 8, No. 6, Jan. 1997, pp. 716–736.
Sitaraman, M., Ogden, W.F., and Weide, B.W., “On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations,” IEEE Trans. Software Engineering, Vol. 23, No. 3, Mar. 1997, pp. 157–170.
Sitaraman, M., Atkinson, S., Kulczycki, G., Weide, B. W., Long, T. J., Bucci, P., Pike, S., Heym, W., and Hollingsworth, J. E., “Reasoning About Software-Component Behavior,” Procs. Sixth Int. Conf. On Software Reuse, IEEE Computer Society Press, Vienna, Austria, June 2000.
Spivey, J. M., The Z Notation: A Reference Manual, Prentice-Hall, 1989.
Szyperski, C., Component Software: Beyond Object-Oriented Programming, Addison-Wesley, 1998.
Weide, B. W., Ogden, W. F., and Sitaraman, M., “Recasting Algorithms to Encourage Reuse,” IEEE Software, Vol. 11, No. 5, Sept 1994, pp. 80–88.
Wing, J. M., “A Specifier’s Introduction to Formal Methods,” IEEE Computer, Vol 29, No. 9, Sept. 1990, pp. 8–24.
Williams, T., “Reusable Components for Evolving Systems,” Proc. 5th Int’l Conf. Software Reuse, IEEE CS Press, 1998, pp. 12–16.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Aronszajn, M., Sitaraman, M., Atkinson, S., Kulczycki, G. (2001). A System for Predictable Component-Based Software Construction. In: Winter, V.L., Bhattacharya, S. (eds) High Integrity Software. The Kluwer International Series in Engineering and Computer Science, vol 577. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1391-9_4
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_4
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive