Specification Construction Using Equivalence Relations and SMT Solvers

الموضوعات

علوم تطبيقية وتكنولوجية

الملخص

We propose an approach to write formal specifications. Our approach partitions the (possibly infinite) state-space of the specification into a finite number of equivalence classes. The partition is defined by the equivalence relation induced by the valuations of a finite set of first-order logic formulae. Our work builds on existing work, which presents a method for writing specifications, along with a preliminary text-based implementation. In this thesis, we extend the current implementation with a graphical-user interface, and use this implementation to conduct experiments with the goal of demonstrating the value of the method by using it to write difficult and intricate specifications, and also using the experimental results as feedback for further improvements to the method.

روابط وملفات

التعريف والنوع

رقم الوثيقة

0f7fb3b4-a6ef-4d2d-b333-308dc2617928

رقم العقد

0

نوع الوسائط

Crawler

نوع المحتوى

الرسائل العلمية

صيغة المصدر

رسائل ماجيستير

نوع الملف

pdf text

أسماء الملفات

1633947_1.pdf

بيانات النشر

ألقاب المؤلفين

[{"name_ar":"Paul Attie","title_ar":"اشراف","title_en":"Supervision"},{"name_ar":"رابح غالب أبو إسماعيل","title_ar":"اعداد","title_en":"Preparation"}]

اللغة

English

المصدر والدورية

اسم المصدر

Specification Construction Using Equivalence Relations and SMT Solvers

المحتوى والصفحات

عدد الصفحات

0

إشراف وإعداد

الإشراف

Paul Attie

الإعداد

رابح غالب أبو إسماعيل

الاقتباسات الببليوغرافية