کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
805495 1468231 2015 11 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Verifying large modular systems using iterative abstraction refinement
ترجمه فارسی عنوان
بررسی سیستم های مدولار بزرگ با استفاده از تکرار انتزاعی تکراری
کلمات کلیدی
چک کردن مدل، تایید، اعتبار سنجی، اصلاح انتزاعی انتزاعی
موضوعات مرتبط
مهندسی و علوم پایه سایر رشته های مهندسی مهندسی مکانیک
چکیده انگلیسی


• We have developed an iterative technique for model checking large modular systems.
• The technique uses BDD-based model checking, k-induction, and PDR in parallel.
• We have tested our algorithm by verifying two models with it.
• The technique outperforms classical model checking methods in our experiments.

Digital instrumentation and control (I&C) systems are increasingly used in the nuclear engineering domain. The exhaustive verification of these systems is challenging, and the usual verification methods such as testing and simulation are typically insufficient. Model checking is a formal method that is able to exhaustively analyse the behaviour of a model against a formally written specification. If the model checking tool detects a violation of the specification, it will give out a counter-example that demonstrates how the specification is violated in the system. Unfortunately, sometimes real life system designs are too big to be directly analysed by traditional model checking techniques. We have developed an iterative technique for model checking large modular systems. The technique uses abstraction based over-approximations of the model behaviour, combined with iterative refinement. The main contribution of the work is the concrete abstraction refinement technique based on the modular structure of the model, the dependency graph of the model, and a refinement sampling heuristic similar to delta debugging. The technique is geared towards proving properties, and outperforms BDD-based model checking, the k-induction technique, and the property directed reachability algorithm (PDR) in our experiments.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Reliability Engineering & System Safety - Volume 139, July 2015, Pages 120–130
نویسندگان
, , ,