Modular Refinement for Submachines of ASMs

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

We describe and formalize a compositional, contract-based submachine refinement for a variant of Abstract State Machines. We motivate the approach by models of the Flash file system case study, where it is infeasible to refine a complete machine as a whole.
published 2014 Proc. of 4th International Conference ABZ 2014

Publisher: Springer

DOI: (Springer Link)


The final publication is available at Springer via 978-3-662-43652-3_16

For questions regarding the publication, please contact!