Оптимизационные процедуры в аффинной проверке моделей
Аннотация
Символьная проверка на модели основана на компактном представлении множеств. На данный момент есть три основных направления символьной проверки моделей: методы, основанные на бинарных разрешающих диаграммах, ограниченная проверка моделей, использующая SAT-решатели, и различные алгебраические подходы к эффективному представлению данных. В данной работе предлагается рассмотреть улучшенные алгоритмы манипуляции с алгебраическим представлением данных, а именно алгоритмы оптимизации аффинных представлений данных.
Список литературы
1. Abdulla P.A., Jonsson B., Nilsson M., Saksena M. A Survey of Regular Model Checking. Proc. of CONCUR'04 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004 // Lect. Notes Comput. Sci. 2004. Vol. 3170. P. 35-48.
2. Bartzis C., Bultan T. Efficient Symbolic Representations for Arithmetic Constraints in Verification // Int. J. Found. Comput. Sci. 2003. Vol. 4. P. 605-624.
3. Boigelot B., Wolper P. Symbolic Verification with Periodic Sets // Lect. Notes Comput. Sci. 1994. Vol. 818. P. 55-67.
4. Boigelot B., Legay A., Wolper P. Iterating transducers in the large // Proc. 15th Int. Conf. on Computer Aided Verification. 2003. Lecture Notes in Computer Science. Vol. 2725. P. 223-235.
5. Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers. 1986. Vol. C-35, №8. P. 293-318.
6. Bultan T., Gerber R., Pugh W. Model Checking Concurrent Systems With Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results // ACM Trans. Progr. Lang, and Systems. 1999. Vol. 21, №4. P. 747-789.
7. Bultan T. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. Proc. of Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 - April 2, 2000 // Lect. Notes Comput. Sci. 2000. Vol. 1785. P. 441-455.
8. Clarke E.M., Grumberg O., Peled D. Model Checking. London: MIT Press, 1999. 314 p.
9. Kozen D. Results on the Propositional Mu-Calculus // Theor. Comput. Sci. 1983. Vol. 27, №3. P. 333-354.
10. McMillan K.L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. 216 p.
11. McMillan K.L. Applying SAT Methods in Unbounded Symbolic Model Checking. Proc. of 14th International Conference, CAV'02, Copenhagen, Denmark, July 27-31, 2002 // Lect. Notes Comput. Sci. 2002. Vol. 2404. P. 250-264.
12. Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Lect. Notes Comput. Sci. 2003. Vol. 2890. P. 395-400.
13. Yavuz-Kahveci T., Bultan T. Heuristics for Efficient Manipulation of Composite Constraints. Proc. of Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8-10, 2002 // Lect. Notes Comput. Sci. 2002. Vol. 2309. P. 57-71.
14. Гаранина Н.О. Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий: дис. ... канд. физ.- мат. наук. Новосибирск, 2004. 172 с.
15. Гаранина Н.О. Аффинное представление данных для проверки моделей программ. Новосибирск, 2004. 48 с. (Препр./ Сиб. отд-ние. РАН. ИСИ; №116.)
16. Гаранина Н.О. Проверка моделей распределенных систем с помощью аффинного представления данных // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С.52-59.
17. http://www.cs.umd.edu/projects/omega/
Рецензия
Для цитирования:
Гаранина Н.О. Оптимизационные процедуры в аффинной проверке моделей. Моделирование и анализ информационных систем. 2011;18(4):56-67.
For citation:
Garanina N.O. Optimization Procedures in Affine Model Checking. Modeling and Analysis of Information Systems. 2011;18(4):56-67. (In Russ.)
Просмотров:
423
Послать статью по эл. почте 