Specification of Viper2 in Z

reportActive / Technical Report | Accession Number: ADA205179 | Open PDF

Abstract:

As a continuation of the use of the specification language Z which was used to specify the Viper 1 microprocessor this paper covers the specification of the Viper 2. This was completed before the definitive HOL specification was complete, therefore there is no proof of correspondence between the two. Using Z did highlight inconsistencies in the HOL specification that may not have appeared until later in the specification. Great Britain.

Author(s):
Kemp, D. H.
Author Organization(s):
ROYAL SIGNALS AND RADAR ESTABLISHMENT MALVERN (UNITED KINGDOM)
Descriptive Note:
Memorandum rept.
Pagination:
0067

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release
Distribution Statement:
Approved For Public Release; Distribution Is Unlimited.

RECORD

Collection: TR
Identifying Numbers
Report Number(s):
RSRE-MEMO-4217
Monitor Series:
RSRE
 Subject Terms
Joint Capability Areas:
JCA_7.1.2_Prevent Non-kinetic Attack; JCA_7.1_Prevent; JCA_7_Protection; JCA_6.4_Information Assurance; JCA_6_Net Centric; JCA_5_Command and Control; JCA_5.2.2_Develop Knowledge and Situational Awareness; JCA_5.2_Understand
Communities of Interest:
No COI(s) Identified
Descriptor(s):
*SPECIFICATIONS, *LANGUAGE, UNITED KINGDOM
Field(s)/Group(s):
Computer Programming and Software
Keyword(s):
FOREIGN REPORTS
Report Date:
1988 Oct 01