Моделирование, сбор и анализ количественных характеристик функционирования распределенных разнородных аппаратно-программных комплексов тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Шмырев, Николай Владимирович

• Шмырев, Николай Владимирович
• кандидат физико-математических наук
• 2009

Оглавление диссертации кандидат физико-математических наук Шмырев, Николай Владимирович

Введение

1 Обзор методов профилирования и моделирования производительности

1.1 Диагностика производительности.

1.2 Направления развития средств профилирования.

1.3 Автоматическое использование данных профилирования

1.4 Управление производительностью.

1.5 Моделирование производительности.

1.6 Проблемы соответствия модели и приложения.

1.7 Программирование, ориентированное на мониторинг.

1.8 Выводы.

2 Моделирование, сбор и анализ количественных характеристик функционирования как аспекты контролируемого выполнения

2.1 Расширение понятия контролируемого выполнения аппаратно-программных комплексов.

2.2 Особенности целевых аппаратно-программных комплексов

2.3 Контролируемое выполнение, основанное на моделировании и верификации.

2.4 Сбор и анализ информации средствами контролируемого выполнения

2.5 Выводы.

3 Моделирование систем и количественных характеристик их функционирования

3.1 Модель распределённых вычислений.

3.1.1 Моделирование разных аспектов вычисления.

3.1.2 Моделирование ресурсов.

3.1.3 Полная модель приложения.

3.2 Моделирование последовательных распределённых приложений

3.3 Автоматизация описания приложения

3.4 Использование ACSL.

3.5 Библиотека моделирования и самоконтроля.

3.5.1 Аннотированная библиотека самоконтроля.

3.5.2 Аннотации к системным функциям взаимодействия потоков и процессов.

3.5.3 Вспомогательные утверждения

3.6 Интеграция со средой разработки приложений

3.7 Выводы.

4 Сбор и анализ количественных характеристик функционирования

4.1 Сбор количественных характеристик.

4.1.1 Архитектура системы профилирования.

4.1.2 Описание компонентов системы профилирования

4.2 Поддержка оптимизации по профилю в компиляторе СКРВ Багет 3.0.

4.3 Выводы.

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

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

Для решения проблем надёжности при разработке ответственных систем применяются модели — формальные спецификации различных аспектов поведения системы. Полное описание поведения серьёзной современной системы в виде единой «монолитной» модели оказывается слишком сложным для разработки и сопровождения. Кроме того, модели систем обычно развиваются эволюционно, путём последовательного уточнения общих описаний вплоть до разработки детальных реализаций (в частности, исходный текст системы на языке высокого уровня может рассматриваться как её модель). Поэтому более практичным представляется подход, при котором описание системы задаётся в виде совокупности моделей, описывающих различные аспекты её поведения, в том числе, потребление ресурсов.

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

Значимость этой проблемы обусловлена тем, что современные системы подвержены постоянным изменениям; изменяется внешняя среда, в которой они работают, модифицируется исходный код, адаптируясь к новым требованиям. При этом могут возникнуть расхождения между различными моделями или между моделями и фактическим поведением системы, что делает результаты моделирования бесполезными. Поэтому актуальной является задача создания методики моделирования и средств верификации, позволяющих эффективно контролировать соответствие моделей системы, её исходного кода и поведения в процессе выполнения.

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

Сложность задачи обеспечения надёжности аппаратно-программных комплексов, многообразие факторов, которые необходимо при этом учитывать, требуют создания целостных подходов к её решению. Таким подходом является концепция контролируемого выполнения, которая направлена на выполнение системой ее миссии, несмотря на наличие ошибок, сбоев аппаратуры, уязвимостей и т.п. Достижение этой цели обеспечивается применением целого спектра средств, таких как мониторинг, интерактивная отладка, детерминированное воспроизведение ошибочных ситуаций в распределённых системах, самоконтроль и др. на протяжение всего жизненного цикла системы, включая этап эксплуатации. Среда контролируемого выполнения, поддерживающая указанные средства, реализована в инструментальном комплексе «СОМ». В контексте данной работы актуальной представляется задача расширения и обобщения концепции контролируемого выполнения путём включения в неё методики контроля за использованием ресурсов, а также реализация соответствующих средств в рамках инструментального комплекса «СОМ».

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

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

Научная новизна. Основные результаты работы являются новыми и заключаются в следующем:

• Концепция контролируемого выполнения существенно расширена и обобщена за счет включения в неё разработанных автором методик моделирования и верификации распределённых разнородных аппаратно-программных комплексов, а также средств сбора и анализа количественных характеристик функционирования таких комплексов.

• Предложены средства построения моделей распределённых разнородных аппаратно-программных комплексов с учётом количественных характеристик их функционирования.

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

Апробация. Основные положения диссертационной работы докладывались на III международной конференции «Параллельные вычисления и задачи управления», Москва, ИПУ РАН, 2006; на VI международной конференции «Идентификация систем и задачи управления», Москва, ИПУ РАН, 2007; на III международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МГУ им. М.В. Ломоносова, 2007; на международной научной конференции «Моделирование-2008», Киев, ИП-МЕ им. Г.Е. Пухова НАН Украины, 2008; на IV международной конференции «Параллельные вычисления и задачи управления», Москва, ИПУ РАН, 2008; на IV международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МГУ им. М.В. Ломоносова, 2008; на VIII международной конференции «Идентификация систем и задачи управления», Москва, ИПУ РАН, 2009; на семинаре «Современные сетевые технологии», МГУ им. М.В. Ломоносова, 2007; на научно-исследовательском семинаре «Проблемы проектирования и реализации базового аппаратно-программного обеспечения» в НИИ системных исследований РАН.

Публикации. По теме диссертации опубликовано 11 печатных работ: [4], [2], [3], [7], [9], [15], [8], [6], [5], [14], [10] из них 10 в соавторстве, 3 в изданиях по перечню ВАК.

Объем и структура работы. Диссертация состоит из введения, 4 глав, заключения и списка литературы.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Шмырев, Николай Владимирович

4.3 Выводы

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

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

Данные профилирования являются важным источником информации для компилятора при принятии решений о целесообразности и параметрах различных оптимизаций. Повышение эффективности кода в результате применения оптимизаций по профилю может составлять в среднем 5 - 20%, а для отдельных программ эффект может быть значительно выше. В настоящее время ведутся активные исследования в области оптимизации по профилю, в частности по такому направлению как динамическая реоптимизация приложений по профилю. В сфере компиляции для встроенных систем развиваются переборные методы адаптивной компиляции, позволяющие подбирать последовательности оптимизаций индивидуально для различных участков программы. В связи с этим интересным направлением исследований представляется интеграция традиционной оптимизации по профилю с переборными методами адаптивной компиляции.

Профилирование является важным аспектом контролируемого выполнения сложных систем. Реализованный в рамках инструментального комплекса СОМ компонент профилирования позволяет эффективно осуществлять настройку приложений для максимального использования аппаратных и программных ресурсов целевой системы. Интеграция профилирования с другими компонентами инструментального комплекса, такими как компонент мониторинга и интерактивной отладки, облегчает процесс сбора необходимой информации и обеспечивает единое централизованное управление всеми компонентами контролируемого выполнения, входящими в состав инструментального комплекса.

Заключение

В диссертационной работе получены следующие основные результаты:

1. Концепция контролируемого выполнения обобщена и распространена на моделирование, сбор и анализ количественных характеристик функционирования распределённых разнородных аппаратно-программных комплексов.

2. Предложены средства построения моделей распределённых разнородных аппаратно-программных комплексов, учитывающих количественные характеристики их функционирования.

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

4. На основании выполненных теоретических и практических разработок произведено расширение инструментального комплекса контролируемого выполнения «СОМ», обеспечена интеграция средств управления и отладки со средствами моделирования, сбора и анализа количественных характеристик функционирования распределённых разнородных аппаратно-программных комплексов.

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

Список литературы диссертационного исследования кандидат физико-математических наук Шмырев, Николай Владимирович, 2009 год

1. Вьюкова Н. И., Галатенко В. А., Малиновский А. С., Шмырев Н. В. Адаптивная компиляция на основе данных профилирования // Информационная безопасность. Технологии программирования / Под ред. Бетелина. — М.: НИИСИ РАН, 2007. — С. 109-124.

2. Вьюкова Н. И., Галатенко В. А., Малиновский А. С., Шмырев Н. В. Адаптивная компиляция на основе данных профилирования // Программные продукты и системы. — 2007. — № 3. — С. 5-8.

3. Вьюкова Н. И., Шмырев Н. В. и др. Описание отладочного комплекса СОМ // Инструментальные средства программирования / Под ред. Бетелина. М.: НИИСИ РАН, 2006. - С. 4-50.

4. Галатенко В. А., Костюхин К. А., Малиновский А. С., Шмырев Н. В. Моделирование и верификация программ как элемент контролируемого выполнения // Программные продукты и системы. — 2008. — № 4. — С. 14-17.

5. Годунов А. Н. и др. Введение в ос2000 // Вопросы кибернетики / Под ред. Бетелина. — М.: НИИСИ РАН, 1999.

6. КБ Корунд-М.— Семейство ЭВМ для специализированных применений, 1997.

7. Костюхин К. А. Организация контролируемого выполнения для разнородных распределенных программно-аппаратных комплексов: Ph.D.thesis / Научно-исследовательский институт системных исследований. — 2006.

8. Костюхин К. А., Малиновский А. С., Шмырев Н. В. Организация профилирования сложных систем в условиях дефицита ресурсов // Программные продукты и системы. — 2008. — № 4. — С. 17-20.

9. Шмырев Н. В. Формальная модель контролируемого выполнения // Технологии программирования. Учетные системы. Ортонормирован-ные системы / Под ред. Бетелина. — М.: НИИСИ РАН, 2008. — С. 141148.

10. Anand М., Kim J., , Lee I. Code generation from hybrid systems models for distributed embedded systems // ISORC. — 2005. — Pp. 28-36.

11. Baudm P., Filliatre J.-C., Marche G. et al— ASCL: ANSI/ISO С Specification Language, 2008.

12. Auguston M., Jeffery C., Underwood S. A framework for automatic debugging // Automated Software Engineering. — 2002. — Pp. 217-222.

13. Auguston M., Jeffery C., Underwood S. A monitoring language for run time and post-mortem behavior analysis and visualization // AADEBUG. — 2003.

14. Benini S. L., Micheli G. D., Hans M. Source code optimization and profiling of energy consumption in embedded systems //In International Symposium on System Synthesis. — 2000. — Pp. 193-198.

15. Beyer D., Henzinger T. A., Jhala R., Majumdar R. Checking Memory Safety with BLAST // FASE'05. — 2005. Pp. 2-18.

16. Beyer D., Henzinger Т., Jhala R., Majumdar R. The Software Model Checker BLAST: Applications to Software Engineering // Int. Journal on Software Tools for Technology Transfer2007.— no. 9(5-6).— Pp. 505525.

17. Binkley D. Source code analysis: A road map // Future of Software Engineering (FOSE). — 2007. — Pp. 104-119.

18. Boldo S., Filliatre J.-G. Formal verification of floating-point programs // CF. 2008.

19. Boronat A., Meseguer J. An Algebraic Semantics for MOF // FASE. — 2008.

20. Brunst H., Knupfer A. — Open Trace Format API Specification. Version 1.1. — http://www.paratools.com/otf/specification.pdf.

21. Burger R. G., Dybvig R. K. An infrastructure for profile-driven dynamic recompilation // In ICCL'98, the IEEE Computer Society International Conference on Computer Languages. — IEEE, 1998.— Pp. 240-251.

22. Carloni L., Benedetto M. D. D., Pinto A., Sangiovanni-Vincentelli A. — Modeling Techniques, Programming Languages, Design Toolsets and Interchange Formats for Hybrid Systems, 2004.

23. Chaki S., Clarke E., Sharygina N. Sinha N. Dynamic component substi-tutability analysis //In Proc. of Conf. on Formal Methods.— Springer Verlag, 2005.-Pp. 512-528.

24. Chanda A., Cox A. L., Zwaenepoel W. Whodunit: transactional profiling for multi-tier applications // SIGOPS Oper. Syst. Rev. — 2007. — Vol. 41, no. 3. Pp. 17-30.

25. Chang P., Mahlke S., Hwu W. Using profile information to assist classic code optimizations I j Software: Practice and Experience. — 1991. — December. — no. 21(12). — Pp. 1301-1321.

26. Chen F., Rosu G. MOP: Reliable Software Development using Abstract Aspects: Tech. rep.: Dept. of Computer Science, University of Illinois, 2006.

27. Chen W. Y. et al. Profile-assisted instruction scheduling // International Journal of Parallel Programming. — 1994. — Vol. 22, no. 2. — Pp. 151-181

28. Compositional quantitative reasoning / K. Chatterjee, L. de Alfaro, M. Faella et al. // ACM. 2007.

29. Cox J., Howel D., Conte T. Commercializing Profile-Driven Optimization // Proceedings of the 28th Annual Hawaii lntemotional Conference on System Sciences. — 1995.

30. Dauphin P. Combining functional and performance debugging of parallel and distributed systems based on model-driven monitoring //In 2nd Eu-romicro Workshop on Parallel and Distributed Processing. — IEEE Computer Society Press, 1994. — Pp. 463-470.

31. Efficient Verification of Sequential and Concurrent С Programs / S. Chaki, E. Clarke, A. Groce et al. // Formal Methods in System Design. — 2004.— Vol. 25, no. 2-3. — Pp. 129-166.

32. End-user tools for application performance analysis using hardware counters / K. London, J. Dongarra, M. S. et al. // International Conference on Parallel and Distributed Computing Systems. — 2001.

33. Espinoza H., Servat D., Gerard S. Leveraging Analysis-Aided Design Decision Knowledge in UML-Based Development of Embedded Systems // SHARK. — 2008.— Pp. 55-62.

34. Experiences and lessons learned with a portable interface to hardware performance counters / J. Dongarra, K. London, S. Moore et al. // IPDPS 2003.— 2003.

35. Filliatre J.-C- Verification of nun-functional programs using interpretations in type theory // J. Functional Programming. — 2003.— Vol. 13, no. 4.— Pp. 709-745.

36. Filliatre J.-C., Marche C. The Why/Krakatoa/Caduceus Platform for Deductive Program Verification // OOPSLA. — 2004.

37. GCC: the GNU Compiler Collection. —http://gcc.gnu.org.

38. Gherbi A., Khendek F. Timed-automata Semantics and Analysis of UML/SPT Models with Concurrency // Proceedings of the 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. — 2007. — Pp. 412-419.

39. GNU binutils home page, — http://www.gnu.org/software/bmutils/binutils.html.

40. Gunter R. Profile driven loop transformations // GCC Developers Summit Procedings. — Ottawa, Ontario, Canada: 2006.— June.

41. Gu G. P., Petriu D. C. From UML to LQN by XML algebra-based model transformations // Proceedings of the 5th international workshop on Software and performance. — 2005. — Pp. 99 110.

42. Hammond K., Ferdinand C., Heckmann R. Towards formally verifiable resource bounds for real-time embedded systems // SIGBED Rev. — 2006. — Vol. 3, no. 4. Pp. 27-36.

43. Havelund К. Run-Time Verification of С Programs // 1st Int. TEST-COM/FATES Conference on Testing of Communicating Systems (TEST-COM) and Formal Approaches to Testing of Software (FATES). — 2008.

44. Havelund K., Wyk E. V. Aspect-Oriented Monitoring of С Programs // EUROMICRO'tM. 2008.

45. Heath M. Т., Malony A. D., Rover D. T. Parallel performance visualization: From practice to theory // IEEE Parallel Distrib. Technol. —1995. — Vol. 3, no. 4. — Pp. 44-60.

46. Henzinger T. A., Alur R. Logics and models of real time // Real Time: Theory in Practice, Lecture Notes in Computer Science.— 1992.— Vol. 600.

47. Henzinger T. A., Horowitz В., Majumdar R., Wong-toi H. Beyond HYTECH: Hybrid systems analysis using interval numerical methods // in HSCC. Springer, 2000. — Pp. 130-144.

48. Henzinger T. A., Sifakis J. The embedded systems design challenge // 14th International Symposium on Formal Methods (FM). — 2006. — Pp. 1-15.

49. Henzinger Т., Kirsch C., Sanvido M., Pree W. From control models to real-time code using Giotto // IEEE Control Systems Magazine. — 2003.— Vol. 23(1).-Pp. 50-64.

50. Herzinger Т., R.Jhalla, R.Majumdar, G.Sutre. Lazy abstraction, principles of programming languages // ACM. — 2002. — Pp. 58-70.

51. Hoare C. A. R. An axiomatic basis for computer programming // Communications of ACM.— 1969. — Vol. 12(10).—Pp. 576-583.

52. Hoskins D. S., Colbourn C. J., Montgomery D. C. Software performance testing using covering arrays // WOSP. — 2005.

53. Hubicka J. Profile driven optimizations in gcc // GCC Developers Summit Procedings. — Ottawa, Ontario, Canada: 2005. — June.

54. Jantsch A., Sander I. Models of computation and languages for embedded system design // IEE Proceedings on Computers and Digital Techniques. — 2005. Pp. 114-129.

55. Jayaputera J., Poernomo I., Schmidt H. Runtime Verification of Timing and Probabilistic Properties using WMI and .NET // EUROMICRO'04. -2004.

56. Jejjry T Russell M. F. J. Scenario-based software characterization as a contingency to traditional program profiling // CASES. — 2002.

57. JML: notations and tools supporting detailed design in Java / G. T. Leavens, K. Rustan, M. Leino et al. // OOPSLA. — 2000. — Pp. 105-106.

58. Jones J., Harrold M. Empirical evaluation of the tarantula automatic fault-localization technique // Proc. of the 20th IEEE/ACM International Conference on Automated Software Engineering.— 2005.

59. JozefH. Extending Hoare logic to Real-Time // Formal aspects of computing. — 1995.

60. Kistler Т., Franz M. Continuous program optimization: A case study // ACM Transactions on Programming Languages and Systems.— 2003.— July. Vol. 25, no. 4. — Pp. 500-548.

61. Lamport L. The temporal logic of actions // ACM Transactions on Programming Languages and Systems. — 1994. — Vol. 16(3). — Pp. 872-923.

62. Lattner C. LLVM: An Infrastructure for Multi-Stage Optimization: Ph.D. thesis / University of Illinois at Urbana-Champaign. — 2002.

63. Lavagno L., Sangiovanni-vincentelli A., Sentovich E. Models of computation for embedded system design //in NATO ASI Proc. on System Synthesis. — Kluwer Academic Publishers, 1998. — Pp. 45-102.

64. Liu Z., Joseph M. Real-Time and Fault-Tolerant Systems. Specification, verification, refinement and scheduling. — UUNU/IIST, 2005.

65. Maier-Komor T.} von Bulow A., Farber G. MetaC and its Use for Automated Source Code Instrumentation of С Programs for Real-Time Analysis // Euromicro Conference on Real-Time Systems. — 2003.

66. Malony A. D., Helm B. R. A theory and architecture for automating performance diagnosis // Future Gener. Comput. Syst.— 2001.— Vol. 18, no. 1.—Pp. 189-200.

67. Malony A. D., Shende S. The TAU Parallel Performance System // International Journal of High Performance Computing Applications. — 2006. — Vol. 20, no. 2.- Pp. 287-311.

68. Management O. — UML Profile for Schedulabibity, Performance and Time Specification, 2005.

69. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. — Springer-Verlag, 1991.

70. Modular Verification of Software Components in С // Transactions on Soft-ware Engineering (TSE).— 2004. — Vol. 30, no. 6. — Pp. 388-402.

71. Monate В., Signoles J. Slicing for Security of Code // Trust '08: Proceedings of the 1st international conference on Trusted Computing and Trust ini Information Technologies. — Berlin, Heidelberg: Springer-Verlag, 2008.— Pp. 133-142.

72. Moseley P., Debray S., Andrews G. Checking program profiles // Third IEEE International Workshop of Source Code Analysis and Manipulation. — 2003.

73. Nicolau A. Run-time disambiguation: coping with statically unpredictable dependencies // ieeetc. — 1989. — May. — Vol. 38. — Pp. 663-678.

74. Object Management Group: Meta Object Facility (MOF) 2.0 Core Specification:. — http://www.omg.org/docs/formal/06-01-01.pdf.85. oprofile home page. — http://oprofile.sourceforge.net.

75. PAPI User's Guide.—http://icl.cs.utk.edu/projects/papi.

76. Parallel Tools Consortium. — http://www.ptools.org.

77. Performance technology for parallel and distributed component software: Research articles / A. Malony, S. Shende, N. Trebon et al. // Concurr. Comput. : Pract. Exper. — 2005. — Vol. 17, no. 2-4. — Pp. 117-141.

78. Pnueli A. The temporal logic of programs // 18th Annual Symposium on Foundations of Computer Science. — 1977. — Pp. 46-57.

79. Profiling tools for hardware/software partitioning of embedded applications // LCTES. — 2003.91. iSchneider F. В., Bloom В., Marzullo K. Putting time into proof outlines // Real-Time: Theory in Practice. — 1992. — Pp. 618-639.

80. Smith C. The evolution of software performance engineering: A survey // IEEE. — 1986.

81. Smith C., Williams L. QSEM: Quantitative Scalability Evaluation Method // IEEE. — 2005.

82. Spear W., Malony A. D., Morris A., Shende S. Integrating TAU With Eclipse: A Performance Analysis System in an Integrated Development Environment // High Performance Computing and Communications.— 2006.- Pp. 230-239.

83. System level performance analysis the SymTA/S approach / R. Henia, A. Hamann, M. Jersak et al. // Computers and Digital Techniques, IEE. — 2005. - Vol. 152. — Pp. 148 - 166.

84. The Coq Proof Assistant. — http://coq.inria.fr.

85. The Frama-C framework for analysis of С code. — http://frama-c.cea.fr/.

86. Truong H.-L., Fahringer T. Self-managing sensor-based middleware for performance monitoring and data integration in grids //19 IEEE International Parallel and Distributed Processing Symposium (IPDPS 2005). — IEEE, 2005.

87. Truong H.-L., Fahringer T. Soft computing approach to performance analysis of parallel and distributed programs // Euro-Par 2005 Parallel Processing. — 2005. — Pp. 50-60.

88. Valgrind home page. — http://valgrind.org.

89. Vetter J. S., Worley P. H. Asserting performance expectations // Super-computing '02: Proceedings of the 2002 ACM/IEEE conference on Su-percomputing. — Los Alamitos, CA, USA: IEEE Computer Society Press, 2002.-Pp. 1-13.

90. Weiss A. R. — Dhrystone Benchmark. White Paper, 2002. — October. — http://www.ebenchmarks.com.

91. Woodside M., Franks G., Petriu D. C. The future of software performance engineering // FOSE '07: 2007 Future of Software Engineering.— Washington, DC, USA: IEEE Computer Society, 2007. — Pp. 171-187.

92. Yi J., Woo H., Browne J. С., Мок A. K. Runtime Verification of Timing and Probabilistic Properties using WMI and .NET // IEEE Real-Time and Embedded Technology and Aplication Symposium. — 2008.