How was solved the "conformance problem" in the AWS s3 implementation?

[gabrielgiussi]

In the twitch presentation Serdar Tarisan mentions the "conformance problem" which is to check the correspondence between the implementation and the design model.

Ankush also talks about this as an unsolved problem in this talk, however Tarisan explains that they use the design "as an executable reference model and run it alongside the implementation code" in what he calls "code conformance check".

Can you explain a bit more of this process? Hot the design becomes an executable reference model? How it runs "alongside" the implementation code?

[amw-zero]

Plus one on this, I came to ask the same question. Can P be used at all to check properties / spec conformance on the implementation level? Or is it primarily targeted at design verification?

[timmyjose]

I would imagine that it's impossible to check the conformance of the implementation against the model, in general. Verification tools like TLA+, P etc. can only explore the model itself. So also for Theorem Provers like Dafny (as shown in the first twitch talk slide) and Isabelle/HOL etc. Unless, of course, your whole software was written in Dafny or Isabelle/HOL, which is not feasible.