کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951820 | 1441618 | 2016 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Modular, crash-safe refinement for ASMs with submachines
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
In this paper we define a formal refinement theory for a variant of State Machines (ASMs) with submachines and power cuts. The theory is motivated by the development of a verified flash file system. Different components of the system are modeled as submachines and refined individually. We define a non-atomic semantics that is suitable for considering power cuts in the middle of operations. We prove that refinement is compositional with respect to submachines and crashes. We give a criterion “crash-neutrality” and corresponding proof obligations that are sufficient to reduce non-atomic reasoning to standard pre/post verification in the context of power failures in file systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 131, 1 December 2016, Pages 3-21
Journal: Science of Computer Programming - Volume 131, 1 December 2016, Pages 3-21
نویسندگان
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif,