کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422475 685094 2008 27 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
ArcAngelC: a Refinement Tactic Language for Circus
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
ArcAngelC: a Refinement Tactic Language for Circus
چکیده انگلیسی

Circus is a refinement language, in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but refinements may be long and repetitive, and using this technique can be hard. Some useful strategies have already been identified, described, and used. By documenting and using them as tactics, a lot can be gained since they can be repeatedly used as single transformation rules. Here, we present ArcAngelC, a language for defining such refinement tactics; we present the language and its application in the formalisation of an existing informal strategy for verification of Ada implementations of control systems.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 214, 28 June 2008, Pages 203-229