Model checking in practice: the T9000 virtual channel processor

Author

Barrett, Geoff

Author_Institution

PACT, Bristol, UK

Volume

21

Issue

2

fYear

1995

fDate

2/1/1995 12:00:00 AM

Firstpage

69

Lastpage

78

Abstract

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. The 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

Keywords

circuit CAD; circuit analysis computing; formal specification; transputers; INMOS CAD system; T9000 virtual channel processor; case study; formal method; industrial products; model checking; nonstandard CSP operators; visual specification style; visual specification styles; Design automation; Design engineering; Design methodology; Geometry; Hardware; Manufacturing processes; Process design; Product design; Refining; Testing;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.345823

Filename

345823