This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Model Checking in Practice: The T9000 Virtual Channel Processor
February 1995 (vol. 21 no. 2)
pp. 69-78
One of the major obstacles to the integration of formal methods in the design of industrial products is the height and gradient of the learning curve. Anything which can alleviate this problem is of enormous benefit. Automatic model checking and visual specification styles provide a gentle introduction to the concept of refinement. This paper presents a case study of the design of the T9000 virtual channel processor as an illustration of the use of some nonstandard CSP operators and a visual specification style. The development which is shown here has been implemented in a single model checking tool which is currently being integrated into the INMOS CAD system.

[1] G. Barrett,“Formal methods applied to a floating-point number system,”IEEE Trans. Software Eng., pp. 611–621, May 1989.
[2] ——,“The fixed point theory of unbounded nondeterminism,”Formal Aspects of Comput., vol. 3, pp. 110–128, 1991.
[3] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[4] M. D. May, G. Barrett, and&D. E. Shepherd,Designing chips that work, pp.3–19,Mechanized reasoning and hardware design, C.A.R. Hoare and M.J.C. Gordon, Eds. Englewood Cliffs, NJ: Prentice-Hall, 1992.
[5] A. W. Roscoe and G. Barrett,Unbounded Nondeterminism in CSP, in Proc. 5th Int. Conf. Math. Foundations of Programming Semantics, New Orleans, LA, Mar. 29–Apr. 1, 1989, LNCS 442, pp. 160--193
[6] D. E. Shepherd and G. Wilson,Making chips that work, New Scientist, vol. 122, no. 1664, May 13, 1989, pp 61–64.

Citation:
Geoff Barrett, "Model Checking in Practice: The T9000 Virtual Channel Processor," IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 69-78, Feb. 1995, doi:10.1109/32.345823
Usage of this product signifies your acceptance of the Terms of Use.