کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
424355 685415 2007 12 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Specification and Generation of Environment for Model Checking of Software Components
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Specification and Generation of Environment for Model Checking of Software Components
چکیده انگلیسی

Model checking of isolated software components is inherently not possible because a component does not form a complete program with an explicit starting point. To overcome this obstacle, it is typically necessary to create an environment of the component which is the intended subject to model checking. We present our approach to automated environment generation that is based on behavior protocols [Plasil, F., and S. Visnovsky, Behavior Protocols for Software Components, IEEE Transactions on Software Engineering, 28(2002)]; to our knowledge, this is the only environment generator designed for model checking of software components. We compare it with the approach taken in the Bandera Environment Generator tool [Tkachuk, O., M. B. Dwyer and C. S. Pasareanu, Automated Environment Generation for Software Model Checking, 18th IEEE International Conference on Automated Software Engineering (ASE03), p. 116, 2003], designed for model checking of sets of Java classes.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 176, Issue 2, 31 May 2007, Pages 143-154