Verification of ASM Refinements Using Generalized Forward Simulation

Простая страница элемента
dc.creatorSchellhorn,Gerhard
dc.date2001
dc.date.accessioned2024-02-06T12:51:25Z
dc.date.available2024-02-06T12:51:25Z
dc.descriptionThis paper describes a generic proof method for the correctness of refinements of Abstract State Machines based on commuting diagrams. The method generalizes forward simulations from the refinement of I/O automata by allowing arbitrary m:n diagrams, and by combining it with the refinement of data structures.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-007-11-0952
dc.identifierhttps://lib.jucs.org/article/27832/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/8037
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 7(11): 952-979
dc.subjectrefinement
dc.subjectforward simulation
dc.subjectdata refinement
dc.subjectcommuting diagrams
dc.subjectAbstract State Machines
dc.subjecttransition systems
dc.subjectI/O-Automata
dc.subjectdynamic logic
dc.subjectcorrectness proofs
dc.subjectinteractive theorem proving
dc.subjectcompiler cerification
dc.titleVerification of ASM Refinements Using Generalized Forward Simulation
dc.typeResearch Article
Файлы
Коллекции
Публикации в журналах НИЯУ МИФИ