FORMAL SPECIFICATION OF THE PROCOS SAFEMOS INSTRUCTION SET

被引：2
作者：
BOWEN, J
机构：
[1] Oxford University Computing Laboratory, Programming Research Group, Oxford, OX1 3QD
来源：
MICROPROCESSORS AND MICROSYSTEMS | 1990年 / 14卷 / 10期
关键词：
MICROPROCESSORS; INSTRUCTION SETS; VERIFICATION; FORMAL METHODS; TRANSPUTERS; OCCAM;
D O I：
10.1016/0141-9331(90)90038-W
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Two collaborative projects, the European ESPRIT BRA ProCoS project and the UK IED safemos project, are currently investigating methods to prove software and hardware systems correct at a number of different levels of abstraction. Both projects intend to concentrate on subsets of Occam, and the transputer instruction set. The projects will aim to use the same machine language so that results obtained on both projects will be compatible. The initial selection of the projects (a simple subset of the transputer) is presented using the specification language Z. The role of the specification in the two projects is explained and the benefits and drawbacks of such a specification are discussed.
引用
收藏
页码：631 / 643
页数：13
相关论文
共 35 条
[1]  
[Anonymous], 1989, Z NOTATION REFERENCE
[2]  
BJORNER D, 1989, EATCS B OCT
[3]  
BOWEN JP, 1987, MICROPROC MICROPROG, V21, P223, DOI 10.1016/0165-6074(87)90042-1
[4]  
BOWEN JP, 1987, PRG60 OXF U PROGR RE
[5]  
BOWEN JP, 1988, 2ND P IEEBCS C SOFTW
[6]  
BOWEN JP, 1990, P PLILP 90 WORKSH PR, P45
[7]  
BOWEN JP, 1990, PJPB23 PROJ DOC
[8]  
COOPER D, 1987, P Z USERS M
[9]   APPLICATION OF FORMAL METHODS TO THE VIPER MICROPROCESSOR [J].
CULLYER, WJ ;
PYGOTT, CH .
IEE PROCEEDINGS-E COMPUTERS AND DIGITAL TECHNIQUES, 1987, 134 (03) :133-141
[10]  
FARR JR, 1987, THESIS OXFORD U UK
1234