You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: Newcastle University » Outputs » Detail

Output details

11 - Computer Science and Informatics

Newcastle University

Return to search Previous output Next output

Output 0 of 0 in the submission

Article title

Mechanising Mondex with Z/Eves

Type

D - Journal article

DOI

10.1007/s00165-007-0059-y

Title of journal

Formal Aspects of Computing

Article number

Volume number

Issue number

First page of article

117

ISSN of journal

1433-299X

Year of publication

2008

URL

http://dx.doi.org/10.1007/s00165-007-0059-y

Number of additional authors

Additional information

<10> Mondex smartcards represented the first EAL7 certified-product, the highest assurance level by international standards, requiring proofs from specification to design to code. This work kick-started the Software Verification Grand Challenge with eight teams using different formalisms, and it took 250 pages of Z specifications. Four residual errors were found and fixed. Its effort served as a comparative measure between methods that has not been performed before. Interestingly, other teams working on simplified versions found most errors. The result: a reference proof and large-scale proof engineering techniques transferred across other GC experiments, and eight other formal methodologies.

Interdisciplinary

Cross-referral requested

Research group

C - Dependability

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract