التحقق أثناء التشغيل

تتطلب واجهة Java IteratorhasNext() استدعاء الدالة وإرجاع القيمة true قبل next()استدعاء الدالة مرة أخرى. إذا لم يحدث ذلك، فمن المحتمل جدًا أن يتجاوز المستخدم نهاية المجموعة . يوضح الشكل على اليمين آلة حالة محدودة تُعرّف مراقبًا محتملاً للتحقق من هذه الخاصية وفرضها باستخدام التحقق أثناء التشغيل. من الحالة غير المعروفة ، يُعد استدعاء الدالة خطأً دائمًا next()لأن هذه العملية قد تكون غير آمنة. إذا hasNext()تم استدعاء الدالة وأرجعت القيمة true ، فمن الآمن استدعاء الدالة مرة أخرى next()، وبالتالي ينتقل المراقب إلى حالة more . أما إذا hasNext()أرجعت الدالة القيمة false ، فلا توجد عناصر أخرى، وينتقل المراقب إلى حالة none . في حالتي more و none ، لا يوفر استدعاء hasNext()الدالة أي معلومات جديدة. من الآمن استدعاء الدالة next()من حالة more ، ولكن يصبح من غير المعروف ما إذا كانت هناك عناصر أخرى، لذا يعود المراقب إلى حالة غير المعروفة الأولية . أخيرًا، يؤدي استدعاء next()الدالة من حالة none إلى الانتقال إلى حالة الخطأ . فيما يلي تمثيل لهذه الخاصية باستخدام منطق زمني خطي بارامتري .

${\displaystyle \forall ~{\text{Iterator}}~i\quad i.{\text{next}}()~\rightarrow ~\odot (i.{\text{hasNext}}()==true)}$

تنص هذه الصيغة على أن أي استدعاء للدالة next()يجب أن يسبقه مباشرةً استدعاء hasNext()لدالة أخرى تُرجع القيمة "صحيح". الخاصية هنا مُعاملة في المُكرِّر i. من الناحية النظرية، يعني هذا وجود نسخة واحدة من المُراقب لكل مُكرِّر مُحتمل في برنامج الاختبار، مع العلم أن أنظمة التحقق أثناء التشغيل ليست مُلزمة بتنفيذ مُراقباتها المُعاملة بهذه الطريقة. سيتم ضبط مُراقب هذه الخاصية لتشغيل مُعالج عند انتهاك الصيغة (أو عند دخول آلة الحالة المحدودة في حالة الخطأ )، وهو ما سيحدث عند next()استدعاء الدالة الأولى دون استدعاء الدالة الثانية أولاً hasNext()، أو عند استدعاء الدالة الأولى hasNext()قبل الدالة الثانية next()، ولكنها أرجعت القيمة "خطأ" .

تتيح فئة Vector في Java طريقتين للتكرار على عناصرها. يمكن استخدام واجهة Iterator، كما رأينا في المثال السابق، أو واجهة Enumeration . بالإضافة إلى إضافة دالة remove لواجهة Iterator، يكمن الاختلاف الرئيسي في أن Iterator "تتعامل مع الأخطاء بسرعة" بينما Enumeration ليست كذلك. هذا يعني أنه في حال تعديل Vector (بغير استخدام دالة remove الخاصة بـ Iterator) أثناء التكرار عليه باستخدام Iterator، سيتم طرح استثناء ConcurrentModificationException . أما عند استخدام Enumeration، فلا يحدث ذلك، كما ذكرنا. قد ينتج عن ذلك نتائج غير حتمية من البرنامج لأن Vector يبقى في حالة غير متسقة من منظور Enumeration. بالنسبة للبرامج القديمة التي لا تزال تستخدم واجهة Enumeration، قد يرغب المستخدم في منع استخدام Enumerations عند تعديل Vector الأساسي. يمكن استخدام النمط المنتظم البارامتري التالي لفرض هذا السلوك:

لكل متجه v ، تعداد e : ( e = v.elements ()) ( e.nextElement ()) ^* v.update () e.nextElement ()

هذا النمط مُعَلم في كلٍّ من التعداد والمتجه. وبشكلٍ بديهي، وكما ذُكر سابقًا، لا تحتاج أنظمة التحقق أثناء التشغيل إلى تنفيذ مراقباتها المُعَلمة بهذه الطريقة، يُمكن اعتبار المراقب المُعَلم لهذه الخاصية بمثابة إنشاء وتتبع نسخة من مراقب غير مُعَلم لكل زوج مُحتمل من المتجه والتعداد. قد تتعلق بعض الأحداث بعدة مراقبات في الوقت نفسه، لذا v.update()يجب على نظام التحقق أثناء التشغيل (نظريًا) إرسالها إلى جميع المراقبات المعنية. هنا، تُحدد الخاصية بحيث تُشير إلى السلوكيات غير الصحيحة للبرنامج. وبالتالي، يجب مراقبة هذه الخاصية للتأكد من مُطابقتها للنمط. يُظهر الشكل على اليمين كود جافا يُطابق هذا النمط، وبالتالي ينتهك الخاصية. يتم تحديث المتجه v بعد إنشاء التعداد e، ثم يُستخدم e.

يُظهر المثالان السابقان خصائص الحالة المحدودة، لكن الخصائص المستخدمة في التحقق أثناء التشغيل قد تكون أكثر تعقيدًا. تُفرض خاصية SafeLock سياسة مطابقة عدد عمليات الحصول على قفل (قابل لإعادة الدخول) وتحريره ضمن استدعاء دالة مُحددة. هذا، بطبيعة الحال، يمنع تحرير الأقفال في دوال أخرى غير تلك التي حصلت عليها، ولكن من المُحتمل جدًا أن يكون هذا هدفًا مرغوبًا فيه للنظام المُختَبَر. فيما يلي مواصفات هذه الخاصية باستخدام نمط سياقي مُعامل:

لكل خيط t ، قفل l : S →ε | S begin( t ) S end( t ) | S l .acquire( t ) S l .release( t )

يحدد النمط تسلسلات متوازنة من أزواج البداية/النهاية المتداخلة وأزواج الاستحواذ/الإفراج لكل مؤشر ترابط وقفل (${\displaystyle \epsilon }$(هي سلسلة فارغة). هنا، تشير البداية والنهاية إلى بداية ونهاية كل دالة في البرنامج (باستثناء استدعاءات الاستحواذ والإفراج). وهما متغيران في Thread لأنه من الضروري ربط بداية ونهاية الدوال إذا وفقط إذا كانت تنتمي إلى نفس Thread. كما أن أحداث الاستحواذ والإفراج متغيرة في Thread لنفس السبب. بالإضافة إلى ذلك، فهما متغيران في Lock لأننا لا نرغب في ربط تحرير قفل واحد باستحواذ قفل آخر. في أقصى الحالات، من الممكن أن يكون هناك مثيل للخاصية، أي نسخة من آلية التحليل الخالية من السياق، لكل تركيبة ممكنة من Thread مع Lock؛ يحدث هذا، مرة أخرى، بشكل بديهي، لأن أنظمة التحقق في وقت التشغيل قد تنفذ نفس الوظيفة بشكل مختلف. على سبيل المثال، إذا كان النظام يحتوي على Threads${\displaystyle t_{1}}$،${\displaystyle t_{2}}$، و${\displaystyle t_{3}}$مزودة بأقفال${\displaystyle l_{1}}$و${\displaystyle l_{2}}$إذاً، من الممكن الاحتفاظ بمثيلات الخصائص للأزواج <${\displaystyle t_{1}}$،${\displaystyle l_{1}}$>, <${\displaystyle t_{1}}$،${\displaystyle l_{2}}$>, <${\displaystyle t_{2}}$،${\displaystyle l_{1}}$>, <${\displaystyle t_{2}}$،${\displaystyle l_{2}}$>, <${\displaystyle t_{3}}$،${\displaystyle l_{1}}$>، و <${\displaystyle t_{3}}$،${\displaystyle l_{2}}$يجب مراقبة هذه الخاصية لرصد أي حالات عدم مطابقة للنمط، لأن النمط يحدد السلوك الصحيح. يوضح الشكل على اليمين مسارًا ينتج عنه انتهاكان لهذه الخاصية. تمثل الخطوات المتجهة للأسفل في الشكل بداية الدالة، بينما تمثل الخطوات المتجهة للأعلى نهايتها. تشير الأسهم الرمادية في الشكل إلى التطابق بين عمليات الحصول على القفل نفسه وتحريره. ولتبسيط الأمر، يُظهر المسار مؤشر ترابط واحدًا وقفلًا واحدًا فقط.

تتطلب مراقبة نظام قيد التشغيل عادةً بعض النفقات الإضافية أثناء التشغيل (قد تُستثنى من ذلك أدوات مراقبة الأجهزة). من المهم تقليل هذه النفقات الإضافية لأدوات التحقق أثناء التشغيل قدر الإمكان، خاصةً عند نشر أدوات المراقبة المُولَّدة مع النظام. تشمل تقنيات تقليل النفقات الإضافية أثناء التشغيل ما يلي:

• تحسين أدوات الرصد . قد يؤدي استخراج الأحداث من النظام قيد التشغيل وإرسالها إلى أدوات المراقبة إلى زيادة كبيرة في الحمل على وقت التشغيل إذا تم ذلك بطريقة غير مباشرة. يُعدّ الرصد الجيد للنظام أمرًا بالغ الأهمية لأي أداة تحقق أثناء التشغيل، ما لم تستهدف الأداة سجلات التنفيذ الموجودة بشكل صريح. توجد العديد من أساليب الرصد المستخدمة حاليًا، ولكل منها مزاياها وعيوبها، بدءًا من الرصد المخصص أو اليدوي، مرورًا بالمكتبات المتخصصة، وصولًا إلى الترجمة إلى لغات البرمجة الموجهة نحو الجوانب، وتوسيع نطاق الآلة الافتراضية، وانتهاءً بالاعتماد على دعم الأجهزة.
• الجمع بين التحليل الثابت والديناميكي . منالأساليب الشائعة في التحقق أثناء التشغيل الجمع بين التحليل الثابت والديناميكي، لا سيما في المترجمات، وذلك لمراقبة جميع المتطلبات التي لا يمكن تلبيتها بشكل ثابت. ويُصبح هذا النهج المزدوج، والمكافئ في نهاية المطاف، هو المعيارفي التحقق أثناء التشغيل، أي استخدام التحليل الثابت لتقليل حجم المراقبة المُرهقة. يُمكن إجراء التحليل الثابت على كلٍ من الخاصية المراد مراقبتها والنظام المراد مراقبته. يُمكن للتحليل الثابت للخاصية المراد مراقبتها أن يكشف عن أحداث معينة غير ضرورية للمراقبة، وأن إنشاء بعض أدوات المراقبة يُمكن تأجيله، وأن بعض أدوات المراقبة الموجودة لن يتم تشغيلها أبدًا، وبالتالي يُمكن حذفها من الذاكرة. يُمكن للتحليل الثابت للنظام المراد مراقبته أن يكشف عن التعليمات البرمجية التي لا يُمكنها التأثير على أدوات المراقبة. على سبيل المثال، عند مراقبة الخاصية HasNext المذكورة أعلاه، لا حاجة لتعديل أجزاء من التعليمات البرمجية حيثيسبق كل استدعاء مباشرةً على أي مسار استدعاءيُرجع القيمة true (كما هو موضح في مخطط تدفق التحكم ).i.next()i.hasnext()
• توليد وإدارة فعّالة للمراقبة . عند مراقبة الخصائص البارامترية، كما في الأمثلة السابقة، يحتاج نظام المراقبة إلى تتبع حالة الخاصية المرصودة بالنسبة لكل حالة من حالات المعامل. نظريًا، يكون عدد هذه الحالات غير محدود، ولكنه عمليًا يكون هائلًا. يتمثل أحد التحديات البحثية المهمة في كيفية توجيه الأحداث المرصودة بكفاءة إلى الحالات التي تحتاجها تحديدًا. ومن التحديات الأخرى ذات الصلة كيفية الحفاظ على عدد هذه الحالات صغيرًا (لتسريع عملية التوجيه)، أو بعبارة أخرى، كيفية تجنب إنشاء حالات غير ضرورية لأطول فترة ممكنة، وكيفية إزالة الحالات التي تم إنشاؤها بالفعل بمجرد أن تصبح غير ضرورية. أخيرًا، تُعمم خوارزميات المراقبة البارامترية عادةً خوارزميات مماثلة لتوليد مراقبات غير بارامترية. وبالتالي، تحدد جودة المراقبات غير البارامترية المولدة جودة المراقبات البارامترية الناتجة. مع ذلك، وخلافًا لأساليب التحقق الأخرى (مثل التحقق من النموذج)، فإن عدد الحالات أو حجم المراقب المولد أقل أهمية في التحقق أثناء التشغيل. في الواقع، قد تحتوي بعض أجهزة المراقبة على عدد لا نهائي من الحالات، مثل حالة خاصية SafeLock المذكورة أعلاه، على الرغم من أن عدد الحالات التي قد تحدث في أي لحظة زمنية يكون محدودًا. المهم هو مدى كفاءة انتقال جهاز المراقبة من حالة إلى أخرى عند تلقيه حدثًا من النظام المُنفِّذ.

من أبرز المعوقات العملية لجميع المناهج الرسمية تردد مستخدميها في تعلم قراءة وكتابة المواصفات، أو جهلهم بها وعدم رغبتهم في ذلك. في بعض الحالات، تكون المواصفات ضمنية، كما هو الحال في حالات الجمود وتضارب البيانات، ولكن في معظم الحالات، يلزم إعدادها. ومن الصعوبات الإضافية، لا سيما في سياق التحقق أثناء التشغيل، أن العديد من لغات المواصفات الحالية لا تتمتع بالقدر الكافي من التعبير عن الخصائص المقصودة.

• صيغ محسّنة. بُذلت جهود كبيرة في مجال التحقق أثناء التشغيل لتصميم صيغ مواصفات تتناسب مع مجالات التطبيق المطلوبة للتحقق أثناء التشغيل بشكل أفضل من الصيغ التقليدية. بعض هذه الصيغ لا تتضمن سوى تغييرات طفيفة أو معدومة في تركيبها، وتقتصر على تغييرات في دلالاتها (مثل دلالات التتبع المحدود مقابل التتبع غير المحدود، إلخ) وفي تنفيذها (آلات الحالة المحدودة المُحسّنة بدلاً من آلات بوشي، إلخ). بينما تُوسّع صيغ أخرى الصيغ الحالية بميزات تُناسب التحقق أثناء التشغيل، ولكنها قد لا تُناسب بسهولة أساليب التحقق الأخرى، مثل إضافة معلمات، كما هو موضح في الأمثلة السابقة. وأخيرًا، هناك صيغ مواصفات صُممت خصيصًا للتحقق أثناء التشغيل، ساعيةً إلى تحقيق أفضل أداء لها في هذا المجال، مع إيلاء اهتمام ضئيل لمجالات التطبيق الأخرى. يُعدّ تصميم صيغ مواصفات أفضل بشكل عام أو أفضل في مجال محدد للتحقق أثناء التشغيل، وسيظلّ، أحد أهم تحديات البحث في هذا المجال.
• الخصائص الكمية. بالمقارنة مع أساليب التحقق الأخرى، يتميز التحقق أثناء التشغيل بقدرته على العمل على قيم محددة لمتغيرات حالة النظام، مما يتيح جمع معلومات إحصائية حول تنفيذ البرنامج واستخدام هذه المعلومات لتقييم الخصائص الكمية المعقدة. لذا، ثمة حاجة إلى لغات خصائص أكثر تعبيرًا تُمكّننا من الاستفادة الكاملة من هذه الإمكانية.
• واجهات مستخدم محسّنة. قراءة وكتابة مواصفات الخصائص ليست بالأمر السهل لغير المتخصصين. حتى الخبراء أنفسهم غالبًا ما يقضون دقائق طويلة في النظر إلى صيغ منطقية زمنية صغيرة نسبيًا (خاصةً عندما تحتوي على عوامل "حتى" متداخلة). من أهم مجالات البحث تطوير واجهات مستخدم فعّالة لمختلف أشكال المواصفات، مما يُمكّن المستخدمين من فهم الخصائص وكتابتها، وربما حتى عرضها بصريًا، بسهولة أكبر.
• استخراج المواصفات. بغض النظر عن أدوات الدعم المتاحة لمساعدة المستخدمين في إنشاء المواصفات، فإنهم غالبًا ما يفضلون عدم كتابة أي مواصفات على الإطلاق، خاصةً عندما تكون بسيطة. لحسن الحظ، توجد العديد من البرامج التي تستخدم الإجراءات/الأحداث التي يرغب المستخدم في الحصول على خصائصها بشكل صحيح. في هذه الحالة، من الممكن الاستفادة من هذه البرامج الصحيحة من خلال التعلم التلقائي للخصائص المطلوبة. حتى لو كان من المتوقع أن تكون الجودة الإجمالية للمواصفات المستخرجة تلقائيًا أقل من جودة المواصفات المُنتجة يدويًا، فإنها يمكن أن تكون بمثابة نقطة انطلاق للمواصفات المُنتجة يدويًا أو كأساس لأدوات التحقق التلقائي أثناء التشغيل، والتي تهدف تحديدًا إلى اكتشاف الأخطاء (حيث تتحول المواصفات الضعيفة إلى نتائج إيجابية أو سلبية خاطئة، والتي غالبًا ما تكون مقبولة أثناء الاختبار).

تعتمد قدرة أداة التحقق أثناء التشغيل على اكتشاف الأخطاء اعتمادًا كليًا على قدرتها على تحليل مسارات التنفيذ. عند نشر أدوات المراقبة مع النظام، يكون استخدام أدوات القياس عادةً في حده الأدنى، وتكون مسارات التنفيذ بسيطة قدر الإمكان للحفاظ على انخفاض الحمل الزائد أثناء التشغيل. عند استخدام التحقق أثناء التشغيل للاختبار، يمكن استخدام أدوات قياس أكثر شمولًا تُضيف إلى الأحداث معلومات نظامية مهمة، والتي يمكن لأدوات المراقبة استخدامها لبناء نماذج أكثر دقة للنظام قيد التنفيذ، وبالتالي تحليلها. على سبيل المثال، يسمح إضافة معلومات ساعة المتجهات ومعلومات تدفق البيانات والتحكم إلى الأحداث لأدوات المراقبة ببناء نموذج سببي للنظام قيد التشغيل، حيث يكون التنفيذ المرصود مجرد حالة واحدة محتملة. أي تبديل آخر للأحداث يتوافق مع النموذج يُعد تنفيذًا ممكنًا للنظام، والذي يمكن أن يحدث في ظل تداخل خيوط مختلف. إن اكتشاف انتهاكات الخصائص في عمليات التنفيذ المستنتجة هذه (عن طريق مراقبتها) يجعل أداة المراقبة تتنبأ بأخطاء لم تحدث في التنفيذ المرصود، ولكنها قد تحدث في تنفيذ آخر لنفس النظام. يتمثل أحد التحديات البحثية المهمة في استخراج النماذج من آثار التنفيذ التي تشمل أكبر عدد ممكن من آثار التنفيذ الأخرى.

على عكس الاختبار أو التحقق الشامل، يُتيح التحقق أثناء التشغيل للنظام إمكانية التعافي من الانتهاكات المكتشفة، من خلال إعادة التكوين، أو إعادة الضبط الجزئي، أو من خلال آليات تدخل أدق تُعرف أحيانًا بالضبط أو التوجيه. ويُثير تطبيق هذه التقنيات ضمن الإطار الصارم للتحقق أثناء التشغيل تحديات إضافية.

• تحديد الإجراءات: يجب تحديد التعديل المطلوب تنفيذه بطريقة عامة لا تتطلب من المستخدم معرفة تفاصيل التنفيذ غير ذات الصلة. إضافةً إلى ذلك، يجب تحديد وقت إجراء هذا التعديل للحفاظ على سلامة النظام.
• التفكير في آثار التدخل. من المهم معرفة أن التدخل يحسن الوضع، أو على الأقل لا يزيد الوضع سوءًا.
• واجهات الإجراءات. على غرار أدوات المراقبة، نحتاج إلى تمكين النظام من استقبال استدعاءات الإجراءات. ستعتمد آليات الاستدعاء بالضرورة على تفاصيل تنفيذ النظام. مع ذلك، على مستوى المواصفات، نحتاج إلى تزويد المستخدم بطريقة تصريحية لتقديم ملاحظات إلى النظام من خلال تحديد الإجراءات التي يجب تطبيقها وشروطها.

أدرك الباحثون في مجال التحقق أثناء التشغيل إمكانية استخدام البرمجة الموجهة نحو الجوانب كتقنية لتعريف أدوات مراقبة البرامج بطريقة معيارية. تُشجع البرمجة الموجهة نحو الجوانب (AOP) عمومًا على تجزئة الاهتمامات المتداخلة. يُعد التحقق أثناء التشغيل أحد هذه الاهتمامات، وبالتالي يمكنه الاستفادة من بعض خصائص البرمجة الموجهة نحو الجوانب. تتميز تعريفات المراقبة الموجهة نحو الجوانب بأنها تصريحية إلى حد كبير، وبالتالي يسهل فهمها مقارنةً بأدوات المراقبة المُعبر عنها من خلال تحويل البرنامج المكتوب بلغة برمجة إجرائية . علاوة على ذلك، يُمكن للتحليلات الثابتة فهم جوانب المراقبة بسهولة أكبر من غيرها من أشكال أدوات مراقبة البرامج، حيث أن جميع أدوات المراقبة مُضمنة ضمن جانب واحد. لذلك، تم تصميم العديد من أدوات التحقق أثناء التشغيل الحالية على شكل مُجمّعات مواصفات، تأخذ مواصفات عالية المستوى كمدخلات وتُنتج كودًا مكتوبًا بلغة برمجة موجهة نحو الجوانب (مثل AspectJ ) كمخرجات.

يمكن للتحقق أثناء التشغيل، عند استخدامه مع كود استعادة صحيح قابل للإثبات، أن يوفر بنية تحتية قيّمة للتحقق من البرامج، مما يقلل بشكل كبير من تعقيدها. على سبيل المثال، يُعد التحقق الرسمي من خوارزمية فرز الكومة أمرًا بالغ الصعوبة. إحدى التقنيات الأقل صعوبة للتحقق منها هي مراقبة مخرجاتها المراد فرزها (مراقبة التعقيد الخطي)، وإذا لم تكن مرتبة، يتم فرزها باستخدام إجراء سهل التحقق، مثل فرز الإدراج. يصبح برنامج الفرز الناتج الآن أسهل في التحقق، والشرط الوحيد المطلوب من فرز الكومة هو عدم إتلاف العناصر الأصلية التي تُعتبر مجموعة متعددة، وهو أمر أسهل بكثير في إثباته. من منظور آخر، يمكن استخدام التحقق الرسمي لتقليل عبء التحقق أثناء التشغيل، كما ذُكر سابقًا بالنسبة للتحليل الثابت بدلًا من التحقق الرسمي. في الواقع، يمكن البدء ببرنامج تم التحقق منه بالكامل أثناء التشغيل، ولكنه قد يكون بطيئًا. ثم يمكن استخدام التحقق الرسمي (أو التحليل الثابت) لإلغاء عمليات المراقبة، بنفس الطريقة التي يستخدم بها المترجم التحليل الثابت لإلغاء فحوصات وقت التشغيل المتعلقة بصحة النوع أو سلامة الذاكرة .

بالمقارنة مع أساليب التحقق التقليدية، يتمثل أحد عيوب التحقق أثناء التشغيل في انخفاض نطاق تغطيته. لا يُشكل هذا مشكلة عند نشر أدوات مراقبة وقت التشغيل مع النظام (مع تضمين رمز استرداد مناسب يُنفذ عند انتهاك الخاصية)، ولكنه قد يُحد من فعالية التحقق أثناء التشغيل عند استخدامه لاكتشاف الأخطاء في الأنظمة. تشمل التقنيات المُستخدمة لزيادة نطاق تغطية التحقق أثناء التشغيل لأغراض اكتشاف الأخطاء ما يلي:

• توليد المدخلات. من المعروف أن توليد مجموعة جيدة من المدخلات (قيم متغيرات إدخال البرنامج، وقيم استدعاءات النظام، وجداول الخيوط، وما إلى ذلك) يمكن أن يزيد بشكل كبير من فعالية الاختبار. وينطبق هذا أيضًا على التحقق أثناء التشغيل المستخدم لاكتشاف الأخطاء، ولكن بالإضافة إلى استخدام كود البرنامج لتوجيه عملية توليد المدخلات، يمكن في التحقق أثناء التشغيل استخدام مواصفات الخصائص، عند توفرها، كما يمكن استخدام تقنيات المراقبة لحث السلوكيات المطلوبة. هذا الاستخدام للتحقق أثناء التشغيل يجعله وثيق الصلة بالاختبار القائم على النموذج، على الرغم من أن مواصفات التحقق أثناء التشغيل عادةً ما تكون عامة الأغراض، وليست بالضرورة مصممة لأغراض الاختبار. لنفترض، على سبيل المثال، أننا نريد اختبار خاصية UnsafeEnum العامة المذكورة أعلاه. بدلاً من مجرد توليد أداة المراقبة المذكورة أعلاه لمراقبة تنفيذ النظام بشكل سلبي، يمكننا توليد أداة مراقبة أكثر ذكاءً تُجمّد الخيط الذي يحاول توليد حدث e.nextElement() الثاني (قبل توليده مباشرةً)، مما يسمح للخيوط الأخرى بالتنفيذ على أمل أن يُولّد أحدها حدث v.update() ، وفي هذه الحالة يكون قد تم العثور على خطأ.
• التنفيذ الرمزي الديناميكي. في التنفيذ الرمزي، تُنفَّذ البرامج وتُراقَب بشكل رمزي، أي دون مدخلات ملموسة. قد يغطي تنفيذ رمزي واحد للنظام مجموعة كبيرة من المدخلات الملموسة. غالبًا ما تُستخدم تقنيات جاهزة لحل القيود أو التحقق من قابلية الإرضاء لتوجيه عمليات التنفيذ الرمزي أو لاستكشاف نطاقها بشكل منهجي. عندما تعجز أدوات التحقق من قابلية الإرضاء الأساسية عن التعامل مع نقطة اختيار، يُمكن توليد مدخل ملموس لتجاوز تلك النقطة؛ويُشار إلى هذا المزيج من التنفيذ الملموس والرمزي أيضًا بالتنفيذ الرمزي الملموس.