How was solved the "conformance problem" in the AWS s3 implementation? #577
Unanswered
gabrielgiussi
asked this question in
Q&A
Replies: 2 comments · 1 reply
|
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? |
1 reply
|
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
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?
All reactions