Documenting and verifying systems assembled from components

Abstract

This paper presents an approach to the problem of documenting the design of a network of components and verifying that its structure is complete and consistent, (i.e., that the components, functioning together, will satisfy the requirements of the complete product), before the components are implemented. Our approach differs from others in that both hardware and software components are viewed as hardware-like devices in which an output value can change instantaneously when input values change and all components operate synchronously rather than in sequence. We define what we mean by completeness and consistency and illustrate how the documents can be used to verify a design before it is implemented.

Keywords

networks of components / completeness / consistency

References

[1] Dijkstra E W. On the role of scientific thought. Selected Writings on Computing: A Personal Perspective. Published by Springer-Verlag, 1982, 60-66

[2] Parnas D L. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 1972, 15(12): 1053-1058

[3] Linger R C, Witt B I, Mills H D. Structured programming: Theory and Practice, The Systems Programming Series, 1st. Addison-Wesley Longman Publishing Co., Inc., 1979

[4] Mills H D. The new math of computer programming. Communications of the ACM, 1975, 18(1): 43-48

[5] D.L. ParnasJ. Madey. Functional documents for computer systems. Science of Computer Programming (Elesevier)1995

[6] Heninger K. Specifying software requirements for complex systems: new techniques and their application. IEEE Transactions on Software Engineering, 1980, SE-6(0): 2-13

[7] Heninger K, Kallander J, Parnas D L, Shore J. Software requirements for the A-7E aircraft, NRL Report 3876, 1978, 523

[8] Parnas D L, Clements P C, Weiss D M. The modular structure of complex systems. IEEE Transactions on Software Engineering, 1985, 11(3): 259-266 (special issue on the 7th International Conference on Software Engineering) Also In: Proceedings of 7th International Conference on Software Engineering, March 1984, 408-417 Reprinted In: Peterson G E (ed.) IEEE Tutorial: “Object-Oriented Computing”, Vol. 2: Implementations. IEEE Computer Society Press, IEEE Catalog Number EH0264-2, 1987, 162-169 Reprinted as Chapter 16 in Ref. [7]

[9] Parnas D L. The use of precise specifications in the development of software. In: Proceedings of IFIP Congress ‘77, North Holland Publishing Company, 1977, 861-867

[10] Parnas D L. Some theorems we should prove. In: Joyce J J, Seger C-J H, eds. Higher Order Logic Theorem Proving and its Applications (6th International Workshop HUG’93), Vancouver, Canada, 1993, 155-162

[11] Parnas D L, Dragomiroiu M. Component interface documentation-using the trace function method (TFM). SQRL paper Aug. 2006 version

[12] Bharadwaj R. Heitmeyer C L. Verifying SCR requirements specifications using state exploration. In: Proceedings of 1st ACM SIGPLAN Workshop on Automatic Analysis of Software, 1997

[13] Heimdahl M P E, Leveson N G. Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 1996, 22(6): 363-377

[14] Heitmeyer C, Labaw B G, Kiskis D. Consistency checking of SCR-style requirements specifications. In: Proceedings of Second IEEE International Symposium on Requirements Engineering, IEEE, New York, 1995, 56-63

[15] Jin M. Table checking tool. Master Thesis, McMaster University, Hamilton, Canada, 2000

[16] Parnas D L, Shore J E, Weiss D. Abstract types defined as classes of variables. In: Proceedings of conference on Data: Abstraction, Definition, and Structure, Salt Lake City, 1976. Reprinted in NRL Memorandum Report 7998, 1976

[17] Zhang J. Search techniques for testing formal specifications. In: Proceedings of 10th Int. Conference on. Software Engineering and Knowledge Engineering, California, USA, 1998

[18] Baber R, Parnas D L, Vilkomir S, Harrison P, O’Connor T. Disciplined methods of software specifications: A case study. In: Proceedings of the International Conference on Information Technology Coding and Computing (ITCC 2005), Las Vegas, NV, USA, IEEE Computer Society, April, 2005

[19] Quinn C, Vilkomir S A, Parnas D L, Kostic S. Specification of software component requirements using the trace function method. In: Proceeding of the International Conference on Software Engineering Advances (ICSEA 2006), Tahiti, French Polynesia, 2006

[20] Wei O. Preliminary requirements checking tool, <DissertationTip/>, McMaster University, Hamilton, Canada, 2001

[21] DeRemer F, Kron H. Programming-in-the-large versus programming-in-the-small. IEEE Transactions on Software Engineering, 1976, SE-2(2): 80-86

[22] Prieto-Diaz R, Neighbors J M. Module interconnection languages. Journal of Systems and Software, 1986, 6(4): 307-334

[23] Tichy W F. Software development control based on module interconnection. In: Proceedings of the 4th IEEE International Conference on Software Engineering, 1979

[24] Allen R, Garlan D. A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology, 1997, 6(3): 213-249

[25] Garlan D, Shaw M. An introduction to software architecture. Advances in Software Engineering and Knowledge Engineering, 1993

[26] Medvidovic N, Taylor R N. A classification and comparison framework for software architecture description languages. IEEE Transactions on Software Engineering, 2000, 26(1): 70-93

[27] Broy M, Denert E, eds. Software Pioneers, Contributions to Software Engineering, Springer, 2002, 728

[28] Parnas D L. A technique for software module specification with examples. Communications of the ACM, 1972, 15(5): 330-336

[29] Bartussek W, Parnas D L. Using assertions about traces to write abstract specifications for software modules, <patent>UNC Report No. TR77-012</patent>, <month>Dec.</month>1977

[30] Parnas D L, Wang Y. Simulating the behaviour of software modules by trace rewriting systems. IEEE Transactions on Software Engineering, 1994, 19(10): 750-759

[31] Wang Y. Specifying and simulating the externally observable behaviour of modules. Doctoral Thesis, McMaster University, Hamilton, Canada, 1994

[32] Parnas D L. On simulating networks of parallel processes in which simultaneous events may occur. Communications of the ACM, 1969, 12(9): 519-531

Acknowledgement

Work was supported by Science Foundation Ireland from 2002 to 2007 under an SFI Fellow appointment.

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg