Please wait a minute...
Shopping Cart Email List Chinese
Advanced Search Fig/Tab
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Featured Articles  |  Most Downloaded  |  Most Reading
Online Submission Subscribe to Our RSS Content Feed
Front Comput Sci Chin    2010, Vol. 4 Issue (2) : 151-161    https://doi.org/10.1007/s11704-010-0026-2
RESEARCH ARTICLE
Documenting and verifying systems assembled from components
Zhiying LIU1(), David Lorge PARNAS1,2(), Baltasar Trancon y WIDEMANN1()
1. Software Quality Research Laboratory, Faculty of Informatics and Electronics, University of Limerick, Limerick, Ireland; 2. McMaster University, Canada
 Download: PDF(192 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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     
Corresponding Author(s): LIU Zhiying,Email:Zhiying.liu@ul.ie; PARNAS David Lorge,Email:parnas@mcmaster.ca; WIDEMANN Baltasar Trancon y,Email:Baltasar.Trancon@ul.ie   
Issue Date: 05 June 2010
 Cite this article:   
Zhiying LIU,David Lorge PARNAS,Baltasar Trancon y WIDEMANN. Documenting and verifying systems assembled from components[J]. Front Comput Sci Chin, 2010, 4(2): 151-161.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-010-0026-2
https://academic.hep.com.cn/fcs/EN/Y2010/V4/I2/151
Fig.1  Four variable view of computer system requirements
Fig.1  Four variable view of computer system requirements
Fig.2  Inputs and outputs of a stack
Fig.2  Inputs and outputs of a stack
Fig.3  “Not gate” in an unstable network
Fig.3  “Not gate” in an unstable network
Fig.4  connected to to produce component
Fig.4  connected to to produce component
Fig.5  and connected to compose
Fig.5  and connected to compose
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
doi: 10.1145/361598.361623
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
doi: 10.1145/360569.360659
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
doi: 10.1109/TSE.1980.230208
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
doi: 10.1109/32.508311
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, , 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
doi: 10.1109/TSE.1976.233534
22 Prieto-Diaz R, Neighbors J M. Module interconnection languages. Journal of Systems and Software , 1986, 6(4): 307-334
doi: 10.1016/0164-1212(86)90002-6
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
doi: 10.1145/258077.258078
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
doi: 10.1109/32.825767
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
doi: 10.1145/355602.361309
29 Bartussek W, Parnas D L. Using assertions about traces to write abstract specifications for software modules, UNC Report No. TR77-012, Dec.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
doi: 10.1145/363219.363233
[1] Chenchen HUANG, Huiqi HU, Xing WEI, Weining QIAN, Aoying ZHOU. Partition pruning for range query on distributed log-structured merge-tree[J]. Front. Comput. Sci., 2020, 14(3): 143604-.
[2] Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[3] Fei WANG, Tieyun QIAN, Bin LIU, Zhiyong PENG. Patent expanded retrieval via word embedding under composite-domain perspectives[J]. Front. Comput. Sci., 2019, 13(5): 1048-1061.
[4] Hailong LIU, Zhanhuai LI, Qun CHEN, Zhaoqiang CHEN. Automatic Web-based relational data imputation[J]. Front. Comput. Sci., 2018, 12(6): 1125-1139.
[5] Shaobo DENG, Sujie GUAN, Min LI, Lei WANG, Yuefei SUI. Decomposition for a new kind of imprecise information system[J]. Front. Comput. Sci., 2018, 12(2): 376-395.
[6] Zhilin LI, Wenbo XU, Xiaobo ZHANG, Jiaru LIN. A survey on one-bit compressed sensing: theory and applications[J]. Front. Comput. Sci., 2018, 12(2): 217-230.
[7] Wei LI, Yuefei SUI. The B4-valued propositional logic with unary logical connectives ∼1 / ∼2 /¬[J]. Front. Comput. Sci., 2017, 11(5): 887-894.
[8] Hao ZHU,Yongming NIE,Tao YUE,Xun CAO. The role of prior in image based 3D modeling: a survey[J]. Front. Comput. Sci., 2017, 11(2): 175-191.
[9] Yu TANG,Hailong SUN,Xu WANG,Xudong LIU. An efficient and highly available framework of data recency enhancement for eventually consistent data stores[J]. Front. Comput. Sci., 2017, 11(1): 88-104.
[10] Quanqing XU , Bin CUI , Yafei DAI , Hengtao SHEN , Zaiben CHEN , Xiaofang ZHOU , . Hybrid information retrieval policies based on cooperative cache in mobile P2P networks[J]. Front. Comput. Sci., 2009, 3(3): 381-395.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed