|
1.2 کار مرتبط
معیار منطق از نظر نحوی (با فرض اینکه یک گزاره در یک قالب خاص است) و معنایی (بدون فرض هیچ‌گونه قالبی) مورد بررسی قرار گرفته است. چایلنسکی و میلر [6] در مورد معیار پوشش تصمیم/ شرایط اصلاح‌شده (MC/DC) بحث کرده‌اند که بهترین معیار منطق معنایی شناخته شده است. با این حال آزمونهای MC/DC تشخیص اکثر نقص‌ها در سلسله‌مراتب نقص‌های لاو و یو را تضمین نمی‌کند [7]. ویووکر ، گورادیا و سینق [13] معیارهای نحوی MAX-A و MAX-B را پیشنهاد دادند، که آزمونهای آن‌ها سبب تضمین تشخیص تمامی نقص‌ها در سلسله مراتب شده است. چن، لاو و یو [4] یک معیار MUMCUT را توسعه دادند که در آن آزمون‌ها سبب تضمین تشخیص تمامی نقص‌ها در سلسله‌مراتبی با اندازه مجموعه آزمون کوچک‌تری شد. چن و لاو [2] الگوریتم حریصانه MUTP را برای برآورده‌سازی معیار MUTP به عنوان مولفه‌اصلی معیار MUMCUT پیاده‌سازی کردند. کامینسکی ، ویلیامز و اممان [7] معیار MUTP/NFP را ارائه کردند که در آن آزمون‌ها سبب تضمین تشخیص تمامی نقص‌ها در سلسله مراتب می‌شود و علاوه بر این سبب کاهش اندازه مجموعه آزمون نیز می‌شد ولی تنها در صورتی که معیار امکان‌پذیر بود. سان و همکاران [12] به تجزیه و تحلیل این پرداختند که چگونه MUMCUT را می‌توان گسترش داد تا بر روی گزاره‌هایی در هر قالبی قابل اعمال باشد و اکون ، بلک و یشا [11] نشان دادند که چگونه یک سلسله‌مراتب نقص منطق را می‌توان در هر گزاره‌ای در هر قالبی اعمال کرد. کار اصلی در تدوین یک سلله مراتب نقص منطقی است که توسط کوهن [8] انجام شده است. لاو و یو کار کوهن را با معرفی نقص‌های جدید و روابط تشخیصی جدید اصلاح کردند.
در این مقاله به بهبود تحقیقات پیشین با تمرکز بر امکان‌سنجی معیار برای اصطلاحات و لیترال‌های تکی پرداختیم. نتیجه معیار جدیدی است که سبب کاهش اندازه مجموعه‌آزمون بدون قربانی‌کردن تشخیص نقص شده است، حتی اگر غیرممکنی برای کل گزاره به وقوع بپیوندد.
2. معیار منطق
اندازه آزمون منطقی جامع، به شکل نمایی رشد می‌کند، آزمونهای مورید نیاز O(2n) است که در آن n تعداد لیترال‌های منحصر به فرد است. آزمایش‌کنندگان معیارهای ارزان‌تری را اختراع کردند. چهار مورد از چنین معیارهایی در مثالی به شکل ab+cd توصیف شده است. خلاصه‌ای از هر کدام به همراه یک معیار منطق جدید در بخش 4 قسمت ضمیمه A ارائه شده است. توجه داشته باشید که برای تمامی این معیارها، اگر غیرممکن بودن به وقوع بپیوندد، آزمونهای انتخاب شده باید نیازمندی‌ها را به طور کامل برآورده کنند.
1 .2 MUTP
چند نقطه درست منحصر‌به‌فرد (MUTP): یک گزاره DNF کمینه از آزمون‌هایی برای یک UTP برای هر اصطلاح داده شده است که در آن تمامی لیترال‌ها در اصطلاح مقادیر 1 و 0 را بدست نیاوردند. یک UTP برای اصطلاح اول باید دارای مقادیر a=1 و b=1 باشد. آزمونهای لازم برای c و d برای هر کدام باید به شکل c=0 و d=1 باشد که به شکل 1101 و 1110 هستند. یک UTP برای اصطلاح دوم باید به شکل c=1 و d=1 باشد. آزمونهای لازم برای a و b هر کدام به شکل a=0 و b=1 است و به شکل 0111 و 1011 هستند. یک مجموعه آزمون به شکل {1101,1110,0111,1011} است.
2 .2 MNFP
چند نقطه غلط نزدیک (MNFP): یک گزاره DNF کمینه از آزمون‌هایی برای یک NPF از هر لیترال داده شده است که در آن تمامی لیترال‌ها از نظر اصطلاح لیترال مقادیر 0 و 1 را کسب نکرده است. یک UTP برای اصطلاح اول باید به شکل a=1 و b=1 باشد. NFPها برای a و b و بنابراین برای c و d هر کدام = 0 و 1 است که به شکل 0101،0110، 1001 و 1010 است. یک UTP برای اصطلاح دوم باید دارای c=1 و d=1 باشد. NFPهای لازم برای c و d و بنابراین برای a و b هر کدام = 0 و 1 است که به شکل 010، 1001، 0110، 1010 باشد. یک مجموعه آزمون به شکل
{0101, 0110, 1001,1010} خواهد بود.
3. 2 CUTPNFP
نقطه درست منحصر‌به‌فرد متناظر با نقطه غلظ نزدیک (CUTPNFP): یک گزاره DNF کمینه از آزمون‌هایی برای هر لیترال یافت‌شده در یک UTP و NFP داده شده است که در آن تنها لیترال تغییر مقدار می‌دهد. یک UTP برای اصطلاح اول باید به شکل a=1 و b=1 باشد. اگر c=0 و d=1 باشد، آزمون‌ها برای ab به شکل 1101، 0101 و 1001 است. یک UTP برای اصطلاح دوم باید دارای مقادیر c=1 و d=1 باشد. اگر a=1 و b=0 باشد، آزمون‌ها برای cd به شکل 1011، 1001 و 1010 خواهد بود. یک مجموعه آزمون به شکل {1101,0101,1001,1011,1010} خواهد بود.
4 .2 MUMCUT
MUTP/MNFP/CUTPNFP (MUMCUT): این مورد معیارهای MNFP، MUTP، CUTPNFP را برآورده می‌کند. 1101 و 1110 UTPهایی برای ab هستند. 0101 و 0110 NFPهایی برای a هستند که متفاوت از یک UTP برای ab تنها در مقدار a هستند. 1001 و 1010 NFPهایی برای b هستند که در یک UTP برای فقط ab در مقدار b متفاوت هستند. 0111 و 1011 UTPهایی برای cd هستند. 0101 و 1001 NFPهایی برای c هستند که از یک UTP از cd تنها در مقدار c تفاوت دارند. 0110 و 1010 NFPهایی برای d هستند که از یک UTP برای cd تنها در مقدار d تفاوت دارند. در NFPهای بالا تنها هر لیترال از نظر جذب مقدار بهره 1 و 0 مطرح نیستند. یک مجموعه آزمون به شکل زیر خواهد بود:
{1101,1110,0101,0110,1001,1010,0111,1011}.
3. آزمونهای منطقی و سلسله مراتب نقص
یک روش برای ارزیابی آزمون‌ها تعیین تعداد نه نقص DNF کمینه در جدول 1 .3 است که یک مجموعه آزمون با تضمین تشخیص است [8,9].
شرایط برای شناسایی LIF در ادامه شرح داده شده است[4]. اگر لیترالی که قرار نبوده در اصطلاح X درج شده باشد، در اصطلاح X خودش یا نقیضش درج شده باشد، پس یک مجموعه از UTPها برای X که در آن تمامی لیترال‌هایی که در X نیستند مقادیر 0 و 1 را کسب می‌کنند خطا را تشخیص می‌دهند. آزمونهای MUTP سبب تضمین تشخیص در یک LIF خواهند شد [4]. با این حال، زمانی که معیار MUTP غیرممکن باشدف یک LRF وجود دارد که آزمونهای MUTP ممکن است آن را شناسایی نکنند (به قضیه 1 .4 نگاه کنید). ab + ac + bc را به عنوان یک LIF در نظر بگیرید که ab~c + ac + bc را تولید می‌کند. معیار MUTP برای ab غیرممکن است زیرا تنها UTP برای ab برابر با 110 است. بنابراین، آزمونهای MUTP مقادیر متناظر LRFها را تشخیص نمی‌دهد که عبارتند از: cb + ac + bc~ و a~c + ac + bc.
آزمونهای MUTP برای شناسایی یک LRF برای یک لیترال تضمین شده است در صورتی که معیار MUTP برای لیترال اصطلاح امکان‌پذیر باشد [7]. در این مورد، لازم است که معیار MUTP و معیار NFP برآورده شود (یک NFP برای هر لیترال در اصطلاح) تا به تضمین تشخیص یک LIF، LRF و LOF در آن اصطلاح است [7]. NFP برای یک لیترال در یک اصطلاح قابل‌اجرای MUTP با NFPهایی برای سایر لیترال‌ها در اصطلاحات قابل‌اجرای MUTP و با NFPهایی در آزمون‌هایی در CUTPNFP یا MNFP است زیرا هر NFP برای تشخیص لیترال یک LOF برای لیترال است[4] . اگر یک اصطلاح MUTP غیرممکن باشد ولی تمامی لیترهای خارجی که نمی‌توانند در یک UTP برای اصطلاح موجود در اصطلاحات تک لیترالی 0 یا 1 باشند، تشخیصLRF همچنان توسط آزمونهای MUTP تضمین شده است. یک LRF شامل جایگزینی یک لیترال با یک لیترال (یا نقیض آن) است که در یک اصطلاح تک لیترالی وجود دارد و نتیجه این امر یک گزاره TOF، LOF یا یک گزاره TRUE خواهد بود. از آنجایی که UTP تضمین‌کننده شناسایی یک TOF [4] است و یک NFP تضمین‌کننده تشخیص یک LOF یا یک نقص را می‌کند که در آن گزاره‌ها در 1 گیر کرده‌اند، مجموعه آزمون MUTP با همپوشانی NFPها تکمیل شده است که تضمین تشخیص LRF را در پی دارد. برای مثال، در a+b، با جایگزینی a با b به یک TOF برای a می‌رسیم و با جایگزینی a با ~b این گزاره برابر با 1 خواهد شد. در ab + c با جایگزینی a با c به یک TOF برای ab می‌رسیم و با جایگزینی a با ~c به یک LOF برای a خواهیم رسید.
شرایط برای شناسایی LRF مطابق با [4] است که در ادامه توصیف شده است. اگر لیترال x در X به طور غیرمستقیم به‌عنوان برخی از سایر لیترال‌ها یا به عنوان نقیض برخی از سایر لیترال‌هایی که در x نیستند پیاده‌سازی شده باشد، سپس هر یک از مواردی که در ادامه ذکر شده است یک خطا را تشخیص می‌دهد: مجموعه‌ای از UTPها برای X که در آن لیترال‌هایی که در X نیستند مقادیر 0 و 1 را کسب می‌کنند. یک مجموعه از NFPها برای x که در آن تمامی لیترال‌هایی که در X نیستند مقادیر 0 و 1 را کسب می‌کنند. یک جفت UTP-NFP که در آن نقاط فقط در مقدار x متفاوت هستند. معیار CUTPNFP به منظور تولید آزمون‌هایی برای شناسایی یک LRF طراحی شده سات ولی زمانی که این امر غیرممکن است موفق به تولید آزمون‌ها نخواهد شد (قضیه 2 .4 را ببینید). با این حال، هنگامی که معیار CUTPNFP غیرممکن باشد، آزمونهای MNFP را می‌توان برای تضمین تشخیص LRF اضافه کرد [4]. abc + abd + ~b~d + ~deرا در نظر بگیرید. معیار CUTPNFP برای b در abc غیرممکن است. تنها UTP برای abc، 11100 است. NFP متناظر 10100 برای b در abc امکان‌پذیر نیست زیرا یک نقطه TRUE است. حال a~ec + abd + ~b~d + ~de LRF را در نظر بگیرید. از آنجایی که معیار CUTPNFP برای b در abc غیرممکن است، LRF با آزمونهای CUTPNFP غیرقابل شناسایی است. یک NFP تکی برای b در abc برای شناسایی یک LRF نیز تضمین نشده است. معیار MNFP نیازمند آن است که NFP 10110 برای b در abc مورد استفاده قرار بگیرد و LRF را شناسایی کند.
شکل 1 .3 سلسله مراتب نقص لاو و یو [9] که بر اساس چگونگی تاثیر امکان‌سنجی معیار بر روی تشخیص نقص اصلاح شده است. یک فلش توپر از یک نقص منبع به یک نقص مقصد نشان می‌دهد که اگر یک آزمون یک منبع نقص را شناسایی کند، همچنین نقص مقصد مربوطه را نیز تشخیص می‌دهد. هنگامی که معیار MUTP غیرممکن است، یک مجموعه آزمونی که تمامی LIFها را شناسایی کرده است، تضمین نمی‌کند که تمامی LRFها را نیز شناسایی کرده باشد. بنابراین فلش توپر بین LIF و LRF در سلسله مراتب لاو و یو به فلش‌هایی نقطه‌چین تغییر یافته است. در سلسله مراتب لاو و یو هیچ فلشی بین LRF و LOF وجود ندارد. یک فلش نقطه‌چین به منظور نمایش زمانی که تشخیص تمامی LIFها تضمین شده است ولی تشخیص تمامی LRFها تضمین نشده است، اضافه شده است، افزایش آزمون‌هایی برای تشخیص LRFهای شناسایی نشده سبب تشخیص تمامی LOFهای متناظر خواهد شد (مگر اینکه معیار CUTPNFP غیرممکن باشد). دلیل آن این است که وقتی معیار MUTP غیرممکن باشد اما معیار CUTPNFP امکان‌پذیر باشد، UTP یک LRF را شناسایی نخواهد کرد اما NFP مربوطه آن را شناسایی خواهد کرد [4].
|