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