This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Specification and Verified Decomposition of System Requirements Using CSP
September 1990 (vol. 16 no. 9)
pp. 932-948

A formal method for decomposing the critical requirements of a system into requirements of its component processes and a minimal, possibly empty, set of synchronization requirements is described. The trace model of Hoare's communicating sequential processes (CSP) is the basis for the formal method. The method is applied to an abstract voice transmitter and describes the role that the EHDM verification system plays in the transmitter's decomposition is described. In combination with other verification techniques, it is expected that this method will promote the development of more trustworthy systems.

[1] J. Jacob, "Security specifications," inProc. IEEE Symp. Security and Privacy, Oakland, CA, Apr. 1988, pp. 14-23.
[2] A. P. Moore, "Investigating formal specification and verification techniques for Comsec software security," inProc. 11th Nat. Computer Security Conf., Oct. 1988, pp. 129-138.
[3] C. T. Sennett, "Tool support for the production of high integrity software," Royal Signals Radar Establishment, England, 89005, Apr. 1989.
[4] J. C. P. Woodcock, "Transaction processing primitives and CSP,"IBM J. Res. Develop., vol. 31, no. 5, Sept. 1987.
[5] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[6] E. R. Olderog and C. A. R. Hoare, "Specification oriented semantics for communicating sequential processes,"ACTA Inform., vol. 23, pp. 9-66, 1986.
[7] C. A. R. Hoare, "A model for communicating sequential processes," inOn the Construction of Programs, R. M. McKeag and A. M. McNaughton, Eds. London, England: Cambridge University Press, 1980, pp. 229-243.
[8] EHDM Specification and Verification System Version 4. 1, User's Guide, Comput. Sci. Lab., SRI International, May 1988.
[9] EHDM Specification and Verification System: Preliminary Definition of the EHDM Specification Language, Comput. Sci. Lab., SRI International, Jan. 1990.
[10] J. van de Snepscheut,Trace Theory and VLSI Design (Lecture Notes in Computer Science 200). New York: Springer-Verlag, 1985.
[11] A. P. Moore, "The specification and verified decomposition of an example communication system," Naval Res. Lab., Tech. Memo. 5540-019:APM:apm, Jan. 1990.
[12] A. P. Moore, "A method for decomposing requirements of systems of communicating components," Naval Res. Lab., Tech. Memo. 5540- 309:APM:apm, Sept. 1989.
[13] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[14] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[15] R. Milner,Communication and Concurrency. Englewood Cliffs, NJ: Prentice-Hall International, 1989.
[16] S. D. Brookes,On the Relationship of CCS and CSP (Lecture Notes in Computer Science 154). New York: Springer-Verlag, 1983.
[17] J. Hooman and W. P. de Roever, "The quest goes on: A survey of proofsystems for partial correctness of CSP," inLecture Notes in Computer Science, vol. 224, New York: Springer-Verlag, 1985.
[18] H. Barringer,A Survey of Verification Techniques for Parallel Programs (Lecture Notes in Computer Science 191). New York: Springer-Verlag, 1985.
[19] C. A. R. Hoare, "A calculus of total correctness for communicating processes,"Sci. Comput. Program., vol. 1, pp. 49-72, 1981.
[20] C. A. R. Hoare, "Specifications, programs and implementations," Programming Research Group, Oxford Univ., Tech. Monograph PRG-29, 1982.
[21] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7, pp. 417-426, 1981.
[22] Z. C. Chen and C. A. R. Hoare, "Partial correctness of communicating sequential processes," inProc. Int. Conf. Distributed Computing, Paris, Apr. 1981.
[23] N. Francez, D. Lehmann, and A. Pnueli, "A linear history semantics for distributed programming,"Trans. Comput. Syst., vol. 32, pp. 25-46, 1984.
[24] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe, "A theory of communicating sequential processes,"J. ACM, vol. 31, no. 3, pp. 560-599, July 1984.
[25] S. D. Brooks and A. W. Roscoe, "An improved failures model for communicating sequential processes," inLecture Notes in Computer Science, vol. 154, New York: Springer-Verlag, 1985, pp. 281-305.
[26] A. W. Roscoe, "A semantics and proof system for communicating processes,"Lecture Notes in Computer Science, vol. 164, New York: Springer-Verlag, 1984, pp. 68-85.
[27] C. A. R. Hoare, "Algebraic specifications and proofs for communicating sequential processes," inLogic of Programming and Calculi of Discrete Design (NATO ASI Series. Vol. F36), M. Broy, Ed. New York: Springer-Verlag, 1987.
[28] D. I. Good, R. M. Cohen, and J. Keeton-Williams, "Principles of proving concurrent programs in Gypsy," Inst. Comput. Sci., Univ. Texas at Austin, Tech. Rep. ICSCA-CMP-15, Jan. 1979.
[29] D. I. Good. R. L. Akers, and L. M. Smith, "Report on Gypsy 2.05," Computational Logic, Inc., Tech. Rep. 1-b, Jan. 1989.
[30] L. Lamport, "The 'Hoare logic' of concurrent programs,"ACTA Inform., vol. 14, pp. 21-37, 1980.
[31] S. Owicki and D. Gries, "Verifying properties of parallel programs: An axiomatic approach,"Commun. ACM, vol. 19, pp. 279-285, May 1976.
[32] G. M. Levin and D. Gries, "A proof technique for communicating sequential processes,"ACTA Inform., vol. 15, pp. 281-302, 1981.
[33] K. R. Apt, N. Francez, and W. P. de Roever, "A proof system for communicating sequential processes,"ACM Trans. Program Lang. Syst., vol. 2, no. 3, pp. 359-385, July 1980.
[34] N. Soudararajan and O. J. Dahl, "Partial correctness semantics for communicating sequential processes," Institute for Informatics, Univ. Oslo, Norway, Res. Rep. 66.
[35] J. Zwiers, W. P. de Roever, and P. van Emde Boas, "Compositionality and concurrent networks," inLecture Notes in Computer Science, vol. 184, New York: Springer-Verlag, 1985, pp. 509-519.
[36] A. W. Bartussek and D. L. Parnas,"Using traces to write abstract specifications for software modules," Univ. North Carolina, Chapel Hill, Rep. TR 77-012, Dec. 1977.
[37] D. L. Parnas and Y. Wang, "The trace assertion method of module interface specification," Queen's Univ., Kingston, Ont., Tech. Rep. 89-261, Oct. 1989.
[38] J. McLean, "A formal foundation for the abstract specification of software,"J. ACM, vol. 31, no. 3, pp. 600-627, July 1984.
[39] J. McLean, "Using trace specifications for program semantics and verification," Naval Res. Lab., Rep. 9033, Apr. 1987.
[40] D. McCullough, "Noninterference and the composability of security properties," inProc. 1988 Symp. Security and Privacy, Oakland, CA, IEEE Comput. Soc., Apr. 1988.
[41] J. C. P. Woodcock, "Transaction processing primitives and CSP,"IBM J. Res. Develop., vol. 31, no. 5, Sept. 1987.
[42] J. Jacob, "On the derivation of secure components," inProc. 1989 Symp. Security and Privacy, Oakland, CA, May 1989.
[43] INMOS Ltd.,Communicating Process Architecture. London, England: Prentice-Hall International, 1988.
[44] P. B. Hansen, "The Joyce language report,"Software Practice and Experience, vol. 19, no. 6, pp. 579-592, June 1989.
[45] P. H. J. van Eijk, C. A. Vissers, and M. Diaz, ed.,The Formal Description Technique LOTOS. New York: Elsevier-North-Holland, 1989.
[46] G. V. Collis and E. J. Kappos, "OCCAM as a hardware description language,"Software Eng. J., pp. 213-219, Nov. 1987.
[47] B. J. Curry, "Language based architecture eases system design-III,"Comput. Design, vol. 23, no. 1, pp. 127-136, Jan. 1984.
[48] R. D. Dowsing, "Simulating hardware structures in OCCAM,"Software Microsyst., vol. 4, no. 4, pp. 77-84, Aug. 1985.
[49] A. W. Roscoe, "Denotational semantics for Occam," inProc. NSF/ SERC Workshop Concurrency (Lecture Notes in Computer Science 197). New York: Springer-Verlag, July 1984.
[50] D. Craigen, "A description of m-Verdi," I.P. Sharp Associates Limited, Tech. Rep. TR-87-5420-02, Aug. 1985.

Index Terms:
specification; verified decomposition; system requirements; CSP; formal method; synchronization requirements; trace model; formal specification; synchronisation; theorem proving.
Citation:
A.P. Moore, "The Specification and Verified Decomposition of System Requirements Using CSP," IEEE Transactions on Software Engineering, vol. 16, no. 9, pp. 932-948, Sept. 1990, doi:10.1109/32.58782
Usage of this product signifies your acceptance of the Terms of Use.