ABSTRACT. In this short talk we present our experience in using VDMSL as tool for understanding a complex requirements specification of our model of the upcoming EMVCo Next Generation Kernel specifications. EMVCo is the consortium including MasterCard, Visa, Amex, etc for worldwide payment systems. It includes the familiar Chip&Pin and contactless protocols, as well as a number of new operational modes, security verification types (including biometric). EMVCo's objective is to ensure the requirements are are safe/correct as possible.

In order to engage them with any findings, a conversation between ourselves and stakeholders within EMVCo sub-groups has been established through formal simulation of specific protocol runs using VDMSL. The results have been productive and substantial: a number of corrections were suggested, and most importantly a large number of hidden assumptions about types, APIs, and other system parts have been carefully documented.

An issue of attempting to apply formal methods to industrial problems is that elegance often needs to be compromised in order to ensure stakeholders notice/accept the formal results: they ought to see what was built as their artefact, rather than a nicer abstraction.

Our aim, which we have achieved, is to influence the specification process prior to public release later in 2018. To date, we have modelled about 75% of the whole EMV kernel, and hope to complete it by the middle of 2018. It comprises 135 modules and 40KLOC in VDMSL, some of which is automatically generated from an XSD/XML data dictionary.

The work unravelled many technical issues in terms of design decisions, identified tool bugs, as well as the limits of Overture as a tool for industrial use at this scale. We hope to discuss these issues and make some useful suggestions.