کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422472 685094 2008 27 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Refinement-Based Verification of Interactive Real-Time Systems
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Refinement-Based Verification of Interactive Real-Time Systems
چکیده انگلیسی

Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with system's requirements. To cover this, we integrate a specification framework with a verification system. Given a system, represented in a formal specification framework Focus, one can verify its properties by translating the specification to a Higher-Order Logic and subsequently using the theorem prover Isabelle/HOL. Moreover, using this approach one can validate the refinement relation between two given systems. The approach uses the idea of refinement-based verification: we see any proof about a system as the proof that a more concrete system specification is a refinement of a more abstract one. The case when one needs to prove a single property of a system specification can also be seen as a refinement relation: this property can be defined as a Focus specification itself and then one needs just show that the system specification is its refinement. The major aspects of this approach are exemplified here by a case study on telematics (electronic data transmission) gateway.

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