Метод синтеза тестов с гарантированной полнотой по модели расширенного автомата

Расширенные автоматы активно используются при построении тестов для программного обеспечения на основе формальных моделей. Однако полнота тестов, построенных по расширенному автомату на основе покрытия путей, переменных и т.п., остается практически неизвестной; более того, как известно, такие тесты не обнаруживают большое количество часто встречающихся функциональных ошибок в программных реализациях системы, поведение которой описано таким расширенным автоматом. В данной работе для построения тестовых последовательностей мы предлагаем использовать шаблонную реализацию расширенного автомата в языке Java. Поскольку программа составлена по шаблону, то ошибки в программе напрямую переносятся на ошибки в расширенном автомате. В работе предлагается метод построения множества тестовых последовательностей, обнаруживающих функциональные ошибки в шаблонной реализации расширенного автомата. На первом шаге тест, построенный по расширенному автомату одним из известных методов, проверяется на полноту относительно ошибок, сгенерированных инструментом $\mu$Java в шаблонной программной реализации. После этого для каждого необнаруженного тестом программного мутанта строится мутант эталонного расширенного автомата; на следующем шаге по некоторой конечно-автоматной абстракции генерируется последовательность, различающая два расширенных автомата (если такая последовательность существует), которая добавляется в строящийся тест. Построенный таким образом тест является полным относительно ошибок, сгенерированных инструментом $\mu$Java. Если соответствующий конечный автомат, построенный посредством моделирования расширенного автомата, получается слишком сложным, или построить такой конечный автомат не представляется возможным, то полнота построенного теста не гарантируется. Однако экспериментально показывается, что исходный тест, расширенный такими различающими последовательностями, обнаруживает значительно больше функциональных ошибок в программных реализациях системы, для которой расширенный автомат используется в качестве спецификации.