ASM Refinement Preserving Invariants

Простая страница элемента
dc.creatorSchellhorn,Gerhard
dc.date2008
dc.date.accessioned2024-02-06T12:56:48Z
dc.date.available2024-02-06T12:56:48Z
dc.descriptionThis paper gives a definition of ASM refinement suitable for the verification that a protocol implements atomic transactions. We used this definition as the basis of the formal verification of the refinements of the Mondex case study with the interactive theorem prover KIV. The refinement definition we give differs from the one we gave in earlier work which preserves partial and total correctness assertions of ASM runs. The reason is that the main goal of the refinement of the Mondex protocol is to preserve a security invariant, while total correctness is not preserved. To preserve invariants, the definition of generalized forward simulation is limited to the use of "small" diagrams, which contain of a single protocol step. We show a technique that allows to use the natural "big" diagrams that consist of an atomic action being refined by a full protocol run.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-014-12-1929
dc.identifierhttps://lib.jucs.org/article/29108/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/9791
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 14(12): 1929-1948
dc.subjectrefinement
dc.subjectforward simulation
dc.subjectdata refinement
dc.subjectcommuting diagrams
dc.subjectAbstract State Machines
dc.subjectMondex
dc.subjectelectronic purses
dc.subjectsecurity
dc.subjectdynamic logic
dc.subjectweakest preconditions
dc.subjectinteractive theorem proving
dc.titleASM Refinement Preserving Invariants
dc.typeResearch Article
Файлы
Коллекции
Публикации в журналах НИЯУ МИФИ