Why formalize (e.g., developing a formal semantics) an existing standard (e.g., as we did with our formalization of the DOM standard)? Of course, there are obvious benefits such as identifying glitches or areas of (unwanted) under-specification, but what are the wider benefits?

Actually, the most important question that needs to be answered is: what is the relation between the formalization of a standard, the official standard, and implementations that claim to conform to the standard. If there is not a strong link between the formalization between all three artifacts, formal proofs based on the formal specification are only of limited value. This is true regardless if the formalization has been developed in a post-hoc reverse-engineering fashion or is part of the official standard.

Actually, most popular technologies are only specified by standards using a semi-formal or, worse, an informal notation. Moreover, the tools used for writing standards only support, if at all, trivial consistency checks. Thus, it is no surprise that such standards usually contain inconsistencies (e.g., different sections of the same standard that contradict each other) or unwanted under-specifications (e.g., where the authors of the standard omit the specification of important properties that the defined API should fulfill).

Even if a standard is developed formally, or contains a (often non-normative) formalization, two important questions arise:

1. to what extent does the formal model comply with the semi-formal parts of the standard, and
2. to what extent does an actual implementation comply with the formal model?

If the formal model was used for verifying properties, one also needs to validate that the real system fulfills the assumptions made during the verification.

Luckily, for many industrial standards, it is common that the standard includes a compliance-test suite, which gives a first hint how to improve the situation: if the formalization is executable, we can execute the test cases on the formal specification to check that the specification complies to the test suite. But can we do more?

Yes, we can. The following figure shows how we can use test and proof (verification) techniques for establishing strong links between formal standards, compliance test suites, and implementations.

In more detail, we can

• use the existing compliance test suite to check that a formalization satisfies the requirements expressed as tests. As compliance testing is usually the way how implementation show that they comply to a standard, this should give us the same guarantees for the formalization.
• use the formalization to analyze the consistency of the standard as well as prove important correctness, safety, or security properties. If our implementation adheres to the standard and fulfills a comprehensive compliance test suite, this should give us a strong guarantee that compliant implementation fulfill these properties as well.
• use the formalization to generate test cased (e.g., using specification-based or model-based test case generation techniques). This will allow us to improve the coverage of the compliance test suite, e.g., by including tests for properties that have been identified during the formal verification of the formal specification.

This approach shows that not only go test and verification hand-in-hand, it also shows that a formalization of a standard can contribute to improving the informal parts of a standard, such as the compliance test suite.

If you are interested in more detail, please have a look at our TAP paper [1], where we report on applying some of these ideas to our formalization of the DOM standard [2].

References