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