کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4951770 1441600 2017 37 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Derivation of algorithmic control structures in Event-B refinement
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Derivation of algorithmic control structures in Event-B refinement
چکیده انگلیسی
The Event-B formalism allows program specifications to be modelled at an abstract level and refined towards a concrete model. However, Event-B lacks explicit control flow structure and ordering is implicitly encoded in event guards. This makes it difficult to identify and apply rules for transformation of Event-B models to sequential code. This paper introduces a scheduling language to support the incremental derivation of algorithmic control structure for events as part of the Event-B refinement process. We provide intermediate control structures for non-deterministic iteration and choice that ease the transition from abstract specifications to sequential implementations. We present rules for transforming algorithmic structures to more concrete refinements. We illustrate our approach by applying our method to the Schorr-Waite graph marking algorithm.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 148, 15 November 2017, Pages 49-65
نویسندگان
, , ,