Usability Requirement of Formal Verification Tools

Rozilawati Razali, Paul Garratt
dx.doi.org/10.17576/apjitm-2012-0102-04

Abstract

Tatatanda formal mengguna simbol dan interpretasi matematik bagi menggambar unsur sistem. Formaliti yang dikenakan oleh tatatanda tersebut memboleh ketepatan dan ketekalan model sistem disah oleh alatan pengesahbetulan. Namun, tatatanda formal secara umum adalah sukar difahami dan diguna. Sebagai instrumen sokongan, alatan pengesahbetulan seharusnya berupaya mengatasi kekangan ini. Kajian ini mempersembah satu kaji selidik yang dilaksana ke atas dua contoh alatan pengesahbetulan yang menyokong tatatanda formal iaitu ProB dan B-Toolkit. Kaji selidik ini bertujuan mengenal pasti ciri kebolehgunaan yang perlu ada pada sesuatu alatan pengesahbetulan. Kaji selidik ini mengguna rangka kerja Cognitive Dimensions of Notations (CD) dan beberapa kriteria yang dicadang oleh piawaian International Organization for Standardization (ISO) sebagai instrumen kajian. Enam puluh tiga peserta memberi maklum balas terhadap kajian ini. Data dianalisis mengguna pendekatan Grounded Theory. Analisis ini memboleh pengenalpastian ciri abstrak dan sifat yang membentuk garis panduan bagi mereka bentuk alatan pengesahbetulan yang berguna. Garis panduan ini meliputi tiga kategori ciri utama iaitu Antara muka, Utiliti dan Pengurusan Sumber. Ciri tersebut diperinci dengan penyataan sifat dan dimensi khusus pelaksanaannya. Garis panduan ini boleh diguna sebagai rujukan oleh pereka bagi mereka bentuk alatan pengesahbetulan yang menggalak penggunaan tatatanda formal.

keyword

Keperluan kebolehgunaan, Alatan pengesahbetulan formal, Kajian empirikal

Area

Software Engineering and Technology