Модификации и реализации FOTL-метода компьютерной верификации алгоритмов, использующих линейное время тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Прокофьева, Евгения Юрьевна

• Прокофьева, Евгения Юрьевна
• кандидат физико-математических наук
• 2004

Оглавление диссертации кандидат физико-математических наук Прокофьева, Евгения Юрьевна

1 Введение

1.1 Общая характеристика работы

1.2 Формальные методы верификации

1.3 Содержание диссертационной работы

2 Временная логика первого порядка FOTL

2.1 Синтаксис и семантика FOTL

2.2 Разрешимость конечно-определяемых свойств

2.3 FOTL-метод.

3 Модификации FOTL-метода

3.1 Расширение языка рассматриваемых формул.

3.2 Свойства внутренних и внешних функций

3.3 Строгие конечные интерпретации.

3.4 Ступенчатые конечные интерпретации

3.5 Ступенчато-строгие интерпретации.

3.6 Отсутствие равенства для абстрактных сортов.

4 Реализация FOTL-метода

4.1 Автоматическая генерация FOTL-формулы, описывающей запуски

4.2 Компьютерные реализации методов элиминации кванторов

4.3 Прототип системы компьютерной верификации систем реального времени

5 Обобщенная задача о железнодорожном переезде

5.1 Постановка задачи GRCP

5.2 Моделизация GRCP.

5.3 Разрешимый класс FOTL для верификации GRCP

5.4 Компьютерная верификация GRCP.

6 IEEE 1394 Root Contention Protocol.

6.1 Неформальное описание IEEE 1394 RCP.

6.2 Моделирование протокола при помощи ASM

6.3 Требования корректности на языке FOTL

6.4 Разрешимость верификации корректности RCP

6.5 Компьютерная верификация протокола.

Введение диссертации (часть автореферата) на тему «Модификации и реализации FOTL-метода компьютерной верификации алгоритмов, использующих линейное время»

Актуальность темы. Процесс создания любого программного обеспечения как привило включает в себя фазу спецификации требований к программному продукту, фазу спецификации системы (алгоритма), фазу разработки (получение из формальных спецификаций системы исполняемого кода) и фазу валидации (обоснование того, что полученный программный продукт удовлетворяет начальным требованиям). Существует два общеизвестных метода валидации программного обеспечения: тестирование и верификация. Первый, наиболее часто используемый, состоит в тестировании (запуске) программы на конечном множестве входных данных и анализе того, удовлетворяет ли результат (выходные данные) требованиям. Второй метод состоит в построении доказательства того, что спецификации алгоритма удовлетворяют спецификациям требований, т.е. для всех допустимых входных данных алгоритм заканчивает работу, и результат удовлетворяет требованиям. С математической точки зрения только верификация является доказательным методом.

С ростом использования программных систем в повседневной жизни возрастает необходимость разработки эффективных методов автоматической верификации программного обеспечения.

Цели работы

1. Реализация прототипа системы компьютерной верификации параметрических алгоритмов реального времени, основанной на FOTL-методе.

2. Апробация этой системы на верификации некоторых существующих систем и протоколов с временными ограничениями.

3. Разработка модификаций FOTL-метода, расширяющих класс проблем, для которых компьютерная верификация является успешной.

Методы исследования. В диссертации для верификации систем реального времени применяется метод, основанный на временной логике первого порядка (First Order Timed Logic, FOTL) и называемый в диссертации FOTL-методом. Основная идея метода заключается в сведении проблемы верификации алгоритма к проверке общезначимости формулы некоторой временной логики первого порядка. Если удается доказать принадлежность этой формулы к разрешимому подклассу, то общезначимость исходной формулы эквивалентна общезначимости формулы смешанной теории сложения вещественных и целых чисел с раздельными переменными. Для проверки последнего используются алгоритмы элиминации кванторов.

Автором разработан пакет программ, реализующий FOTL-метод, с использованием систем компьютерной алгебры Reduce [59] и QepcadB [58]. Проведены эксперименты с различными реализациями алгоритмов элиминации кванторов для использования в разрабатываемой системе. Экспериментально показана необходимость улучшения метода, так как на длинных формулах он не может быть завершен из-за недостатка памяти или времени при применении методов элиминации кванторов. Разработаны и реализованы модификации основного алгоритма FOTL-метода, сводящие задачи верификации к формулам с меньшим числом связанных переменных. С применением разработанного пакета программ доказана корректность двух систем реального времени.

Научная новизна. Разработан прототип системы компьютерной верификации алгоритмов, использующих линейное время. Эта система позволяет описывать задачи верификации для систем с параметрами, как вещественными, например, временными параметрами системы, так и целыми, например, количеством взаимодействующих процессов. Верификация в предложенной системе не зависит от конкретных значений этих параметров.

Разработанные модификации значительно расширяют круг задач, для которых компьютерная верификация является успешной.

С помощью разработанного пакета программ реализована компьютерная верификация двух систем реального времени: обобщенной задачи о железнодорожном переезде и протокола выбора лидера из двух конфликтующих процессов стандарта IEEE 1394. Кроме того, что названные системы имеют конкретные практические приложения, они так же являются примерами для сравнения различных систем автоматической верификации алгоритмов. Впервые рассматриваемые задачи проанализированы во всей полноте, т.е. доказательство учитывает все параметры. Получены необходимые и достаточные условия, которым должны удовлетворять параметры этих систем для обеспечения их корректности.

Практическая ценность. Разработанная система может быть использована для компьютерной верификации ряда алгоритмов, например, в системах реального времени с параметрами.

Список литературы диссертационного исследования кандидат физико-математических наук Прокофьева, Евгения Юрьевна, 2004 год

1. Д. Бокье, Е. Прокофьева. Реализация основного этапа алгоритма проверки существования модели заданной сложности для формул некоторой временной логики. 1. Труды V-й молодежной научной школе по дискретной математике и её приложениям, Пенза, Россия, 2001.

2. Д. Бокье, Е. Прокофьева. Применение метода элиминации кванторов в задачах анализа алгоритмов. In Региональная Информатика (РИ-2002), Санкт-Петербург, Россия, 2002.

3. Н.К. Косовский, Е.Ю. Прокофьева. Реализация алгоритма разрешимости теории вещественного сложения. In Региональная Информатика (РИ-2000), Санкт-Петербург, Россия, 2000.

4. Э. Энгелер. Метаматематика элементарной математики. Москва "Мир", 1987. перевод с немецкого 31] Г.Е. Минца под редакцией А.О. Слисенко.

5. М. Archer and С. Heitmeyer. Mechanical verification of timed automata: A case study. Technical Report 5546-98-8180, University Paris-12, Department of Informatics, Naval Reserach Laboratory, Washington, 1998. NRL Memorandum Report.

6. G. Bandini, R. L. Spelberg, R. С. H. de Rooij, and H. Toetenel. Application of parametric model checking the root contention protocol. In Sixth Annual Conference of the Advanced School for Computing and Imaging(ASCI 2000), Lommel, Belgium, June 2000.

7. D. Beauquier and E. Prokofieva. A logical framework for an automatic verification of ieee 1394a root contention protocol. In 8th International Conference on Applications of Computer Algebra (АСА 2002), pages 22-23, Volos, Greece, June 2002.

8. D. Beauquier and A. Slissenko. Decidable classes of the verification problem in a timed predicate logic. Fundamentals (or Foundations) of Computation Theory, 12, 1999.

9. D. Beauquier and A. Slissenko. A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic, 113:13-52, 2002.

10. D. Beauquier and A. Slissenko. Periodicity based decidable classes in a first order timed logic. Technical Report 2004-04, University Paris 12, Department of Informatics, 2004. Available at http://www.univ-parisl2.fr/lacl/.

11. L. Berman. The complexity of logical theories. Theoretical Computer Science, 11:71— 77, 1991.

12. N. Bjorner, Z. Manna, H. Sipma, and T. Uribe. Deductive verification of real-time systems using STeP. Technical Report STAN-CS-TR-98-1616, Computer Sci. Dept., Stanford Univ., December 1998. Submitted to Elsevier Science.

13. C. Brown. Implementing Q.E. by CAD to be compleye, correct, fast and "good". In 8th International Conference on Applications of Computer Algebra (АСА 2002), page 23, Volos,Greece, June 2002. University of Thessaly.

14. Christopher W. Brown. An overview of QEPCAD B: a tool for real quantifier elimination and formula simplification. Journal of Japan Society for Symbolic and Algebraic Computation, 10(l):13-22, 2003.

15. Christopher W. Brown. QEPCAD B: a program for computing with semi-algebraic sets using cads. SIGSAM Bull., 37(4):97-108, 2003.

16. J. Buchi. Weak second-order arithmetic and finite automata. Z.Math. Logik Grundlagen Math., 6:66-92, 1960.

17. F. Budan de Boislaurent. Nouvelle methode pour la resolution des equation numeriques d'un degre quelconque,1807. Paris, 1822. 2nd edition.

18. A. Bundy and I. Green. A comparison of decision procedures in presburger arithmetic, November 1999. The Pennsylvania State University CiteSeer Archives.

19. G. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. Lecture Notes in Computer Science, 33:134-183, 1975.

20. G. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12(3), Septembre 1991.

21. A. Collomb-Annichini and M. Sighireanu. Parametrized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX. In Proceedings of the Workshop on Real-Time Tools (RT-TOOLS'2001), 2001.

22. D. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91-99, 1972.

23. R. Descartes. La geometrie livre iii. OEuvres des Descartes, 6:442-485, 1973.

24. A. Dolzmann and T. Sturm. Redlog user manual. Technical Report MIP-9905, Universitat Passau, April 1999.

25. E. Engeler. Metamathematik der Elementarmathematik. Hochschultext. Springer-Verlag, Berlin Heidelberg New York, 1983.

26. M. Fischer and M. Rabin. Super-exponential complexity of presburger arithmetic. In Symp. on appl. Math., volume 7 of SIAM-AMS Proc., pages 27-41, 1974.

27. J.-B. Fourier. Analyse des equation determinees. F. Didot, Paris, 1831.

28. V Ganesh, S. Berezin, and D. Dill. Deciding presburger arithmetic by model checking and comparisons with other methods. In FMCAD'02, 2002.

29. Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Borger, editor, Specification and Validation Methods, pages 9-93. Oxford University Press, 1995.

30. A. Hearn. REDUCE user's and contributed packages manual, version 3.7. Available from Konrad-Zuse-Zentrum Berlin, Germany, February 1999.

31. C. Heitmeyer, R. Jeffords, and B. Labaw. A benchmark for comparing different approaches for specifying and verifying real-time systems. In Proc. of the 10th IEEE Workshop on Real-Time Operating Systems and Software, New York. IEEE, 1993.

32. C. Heitmeyer and N. Lynch. The generalized railroad crossing: a case study in formal verification of real-time systems. In Proc. of Real-Time Systems Symp., San Juan, Puerto Rico. IEEE, 1994.

33. C. Heitmeyer and D. Mandrioli, editors. Formal Methods for Real-Time Computing, volume 5 of Trends in Software. John Wiley & Sons, 1996. Series Editor: B. Krishnamurthy.

34. L. Hodes. Solving problems by formula manipulation in logic and linear inequalities. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 553-559, London, England, 1971. Imperial College.

35. T. Hune, J. Romijn, M. Stoelinga, and F. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, 2002.

36. Institute of electrical and electronic engineers. IEEE Standart for a High Performace Serial Bus. Std 1394-1995, August 1995.

37. Institute of electrical and electronic engineers. IEEE Standart for a High Performace Serial Bus Amenedement 1. Std 1394a-2000, June 2000.

38. F. Klaedtke. On the automata size for presburger arithmetic. In 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pages 110-119, Turku, Finland, July 2004. IEEE Computer Society Press.

39. Mathematica. Web-site: http://www.wolfram.com/products/mathematica/.

40. Microsoft Visual С++ 6.0 Introductory Edition. Wrox Press et Editions Eyrolles, 1999.2 p*n

41. D. Oppen. A 2 upper bound on the complexity of presburger arithmetic. Journal of Logic and Algebraic Programming, 1978.

42. M. Presburger. Uber de vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt. In Sprawozdanie z I Kongresu metematykow slowinskich, Warszawa 1929, pages 92-101, Warsaw, 1930.

43. M. Presburger. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. History and Philosophy of Logic, 12:225-233, 1991. (Translation of 52] by D. Jacquette).

44. E. Prokofieva. Expiriments with automatic verification of GRCP and IEEE 1394 RCP. Available at http://www.univ-parisl2.fr/lacl/prokofieva.

45. E. Prokofieva. A program of solvability of linear equality and inequality systems with parameters. In 6th IMACS International Conference on Applications of Computer Algebra (IMACS АСА 2000), page 62, Saint-Petersburg, Russia, June 2000.

46. W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Technical report, 1991.

47. Qepcad. Web-site: http://www.cs.usna.edu/ qepcad.

48. QepcadB. Web-site: http://www.cs.usna.edu/ qepcad/b/qepcad.html.

49. Reduce. Web-site: http://www.reduce-algebra.com/ and http://www.uni-koeln.de/reduce/.

50. A. Seidl. Cylindrical algebraic decomposition for real quantifier elimination within redlog. In 8th International Conference on Applications of Computer Algebra (АСА 2002), page 35, Volos,Greece, June 2002. University of Thessaly.

51. N. Shankar. Verification of real-time systems using PVS. In Proc. 5th International Computer Aided Verification Conference, pages 280-291, 1993.

52. D. Simons and M. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using UppaaJ2k. Springer International Journal of Software Tools for Technology Transfer, pages 469-485, 2001.

53. T. Skolem. Uber einige stazfunktionen in der arithmetik. In Shifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I. Matematiks naturvidenskapeling klasse, volume 7, pages 1-28, Oslo, 1931.

54. T. Skolem. Uber einige stazfunktionen in der arithmetik. In J. Fenstad, editor, Selected Works in Logic, pages 281-206. Universitetsforlaget, Oslo, 1970. Reprint of the article 63].

55. M. Stoelinga. Fun with FireWire: Experiments with verifying the IEEE 1394 Root Contention Protocol. In J.M.T. Romijn S. Maharaj, C. Shankland, editor, Formal Aspects of Computing, volume 14, page 9, 2002.

56. M. Stoelinga and F. Vaandrager. Root contention in IEEE 1394. In J.-P. Katoen, editor, Proceedings of the 5th AM AST Workshop on Real-Time and Probabilistic Systems (ARTS'99), pages 53-75, Bamberg, Germany, May 1999.

57. A. Strzebonski. Solving systems of strict polynomial inequalities. Journal of Symbolic Computation, 29:471-480, 2000.

58. J. Sturm. Memoire sur la resolution des equation numeriques. In Memoires presentes par divers Savant etrangers a I'Academie royale des sciences, section Sc. math, phys., pages 273-318, 1835.

59. A. Tarski. A decision method of elementary algebra and geometry. Technical report, RAND, Santa Monica, С A, 1948.

60. A. Tarski. A decision method of elementary algebra and geometry. Berkely: University of California Press, 1951.

61. H. Toetenel, R.L. Spelberg, and G. Bandini. Parametric verification of the IEEE 1394a root contention protocol using LPMC. In Seventh International Conference on Real-Time Systems and Applications (RTCSA'OO), Cheju Island, South Korea, December 2000.

62. V. Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5(l-2):3-27, February-April 1988.

63. V. Weispfenning. Quantifier elimination for real algebra the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing, 8(2):85-101, February 1997.

64. V. Weispfenning. Mixed real-integer linear quantifier elimination. In Proc. of the 1999 Int. Symp. on Symbolic and Algebraic Computations (ISSAC'99), pages 129-136. ACM Press, 1999