کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
424484 | 685474 | 2006 | 16 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method ⋆
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
The OTS/CafeOBJ method can be used to model, specify and verify distributed systems. Specifications are written in equations, which are regarded as rewrite rules and used to verify specifications. The usefulness of the method is demonstrated by applying the method to nontrivial problems such as electronic commerce protocols and railroad signaling systems. In this paper we describe a toolkit called Buffet, which assists verification in the method. Given predicates used to split cases and lemmas, Buffet automatically generates proofs (called proof scores) and checks the proof scores using the CafeOBJ system. Buffet also has facilities to display proof scores generated and verification results on a web browser.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 147, Issue 1, 31 January 2006, Pages 57-72
Journal: Electronic Notes in Theoretical Computer Science - Volume 147, Issue 1, 31 January 2006, Pages 57-72