УСТРОЙСТВО ФОРМАЛЬНОЙ ПРОВЕРКИ СОГЛАСОВАННОСТИ УПРАВЛЯЮЩЕЙ ПРОГРАММЫ МИКРОКОНТРОЛЛЕРНОЙ СИСТЕМЫ ЗАДАННОЙ СПЕЦИФИКАЦИИ

Настоящая полезная модель относится к устройствам автоматической проверки корректности систем управления и может быть использована в процессе разработки управляющих программ микроконтроллерных систем.
Проблема проверки корректности работы разрабатываемых микроконтроллерных систем управления в современном мире имеет очень высокую актуальность, поскольку микроконтроллерные системы составляют большую часть встраиваемых систем. Особенную важность настоящее устройство имеет в тех областях, в которых высока цена ошибки, например, таких, как системы управления транспортными средствами, медицинское оборудование, встраиваемые системы безопасности, автоматизированные системы на ответственных объектах и т.д. Критичность любой ошибки в такой системе обуславливает необходимость создания особых средств контроля корректности разрабатываемых систем и средств их проверки их согласованности.
Наиболее близким к заявленному техническому решению является автоматизированное устройство для тестирования микропроцессорных систем (RU 2392657, G06F 11/22, 2010). Однако стандартное тестирование не обеспечивает гарантии отсутствия ошибок в системе, поэтому реализация разрабатываемого устройства предполагает формальную проверку модели для автоматической проверки согласованности программных систем, позволяющую проверить, удовлетворяет ли заданная модель системы формальным спецификациям (Hoffman L. Q&A Talking Model-Checking Technology, Communications of the ACM, 2008).
Замена стандартного блока тестирования на блок формальной проверки модели для проверки согласованности разработанной программы микроконтроллерной системы предполагает проведение следующих этапов работ: составление модели проверяемой системы, составление спецификации как набора проверяемых ограничений, непосредственное применение устройства для проверки заданной модели ее спецификации, получение обработанных результатов проверки. Фиг.1 иллюстрирует общий алгоритм работы систем при реализации формальной проверки модели. В качестве модели может выступать любая программа, написанная по технологии автоматного программирования, которая является эффективной для построения моделей реактивных систем и систем логического управления (А.А.Шалыто Автоматное программирование, Научно-технический вестник Санкт-Петербургского государственного Университета информационных технологий, механики и оптики, Выпуск 53, Санкт-Петербург, 2008).
Техническим результатом предлагаемого устройства является расширение функциональных возможностей процессов выявления ошибок в управляющих программах микроконтроллерных систем за счет обеспечения формальной проверки модели управляющей программы на соответствие разработанной спецификации, которая может составляться в терминах темпоральной логики, что позволяет охватить недоступную для стандартных тестирующих устройств область проверки корректности программ. Под спецификацией на фиг.1 понимается совокупность правил (ограничений, свойств) модели, описанных в терминах предметной области к которой относится объект управления микроконтроллерной системы, выполнимость которых проверяется блоком проверки согласованности. Результатом проверки согласованности является утверждение о теоретической корректности микроконтроллерной системы или обратное утверждение в случае возможности происхождения в проверяемой системе ошибок при исполнении в реальных условиях, а также выдача рекомендаций пользователю в терминах предметной области, к которой относится объект управления. Среди прочих особенностей устройства необходимо выделить такую отличительную функциональную возможность устройства как выдача рекомендаций пользователю в форме процедур согласования микроконтроллерной системы управления и заданной спецификации в терминах предметной области, к которой относится объект управления.
Технический результат достигается за счет того, что в устройство для тестирования микропроцессорных систем, включающее модуль тестирования, блок оперативного хранения данных, блок управления, блок обработки результатов проверки, где блок управления первым своим выходом подключен к блоку оперативного хранения данных, а вторым выходом к блоку обработки результатов проверки, интерфейсный распределительный блок связан управляющим выходом с блоком управления и информационным входом с блоком обработки результатов проверки, вносятся следующие изменения:
1) в качестве блока проверки согласованности модели программы и спецификации вместо модуля тестирования используется модуль формальной проверки модели, подключенный к блоку оперативного хранения данных для хранения промежуточных результатов;
2) в качестве блока управления используется микроконтроллер, осуществляющий перенос информации из блоков ввода модели программы и блоков ввода спецификации программы в блок оперативного хранения данных, запускающий процесс выполнения проверки в модуле формальной проверки программы, а также процесс по обработке полученных от модуля проверки модели результатов, выполняемый блоком обработки результатов проверки;
3) для обеспечения интерфейса с внешним оборудованием выступает интерфейсный распределительный блок, подключенный к блоку ввода модели программы, блоку ввода спецификации программы и блоку обработки результатов проверки, при этом в устройстве отсутствует блок постоянного хранения данных, поскольку модель программы со спецификацией поступают от управляющего вычислительного устройства через интерфейсный распределительный блок, а результаты обработки проверки через данный блок направляются обратно управляющему вычислительному устройству;
4) блок обработки результатов проверки переводит результаты проверки согласованности управляющей программы микроконтроллерной системы заданной спецификации на язык заданной предметной области, к которой относится объект управления.
На фиг.2 приведена функциональная схема устройства. Здесь двойными стрелками обозначено прохождение информационных сигналов, а одинарными стрелками - сигналов управления. Как видно из фиг.2, устройство состоит из интерфейсного распределительного блока 101, блока ввода спецификации программы 102, блока ввода модели программы 103, блока управления 100, блока формальной проверки модели 104, блока оперативного хранения данных 105 и блока обработки результатов проверки 106, первый и второй выходы интерфейсного распределительного блока подключены ко входам блока ввода модели и блока ввода спецификации соответственно, выход блока обработки результатов проверки подключен ко входу интерфейсного распределительного блока, первый и второй информационные входы блока управления подключены к выходам блокам ввода модели программы и спецификации соответственно, первый информационных выход блока управления подключен к блоку оперативного хранения данных, второй информационный выход блока управления подключен к блоку обработки результатов проверки, модуль формальной проверки модели и вход блока обработки результатов проверки подключены к блоку оперативного хранения данных, первый управляющий выход интерфейсного распределительного блока подключен ко входу блока управления, а первый и второй управляющие выходы блока управления подключены к модулю формальной проверки модели и блоку обработки результатов проверки соответственно.
Предполагается подключение настоящего устройства через интерфейсный распределительный блок 101 к управляющему вычислительному устройств. В качестве управляющего вычислительного устройства может выступать, но не в ограничительном смысле, вычислительное устройство общего назначения, вычислительное устройство повышенной производительности. Задачей интерфейсного распределительного блока является распределение данных модели и спецификации, поступающих на его вход со стороны управляющего устройства, на блок ввода модели программы 102 и блок ввода спецификации программы 103 соответственно, а также отправка результирующих данных от блока обработки результатов проверки 106 управляющему вычислительному устройству после завершения работы модуля проверки.
Работа устройства заключается в осуществлении следующих шагов и вложенных в них циклов. На первом шаге производится передача модели и спецификации программы от управляющего вычислительного устройства в интерфейсный распределительный блок настоящего устройства 101 (команда №1, подписанная шрифтом курсивом на фиг.2). На втором шаге (команды №2) интерфейсный распределительный блок распределяет полученную модель и спецификацию и направляет их параллельно в блок ввода модели 102 и блок ввода спецификации 103 соответственно, также на этом шаге интерфейсный распределительный блок оповещает по управляющему выходу блок управления 100 для ожидания данных от блоков ввода модели и спецификации. На третьем шаге (команды №3) блоки ввода модели и спецификации, выполнив необходимые преобразования над данными модели и спецификации, направляют их на ожидающий от них данные блок управления. На четвертом шаге (команда №4) блок управления, выполнив инициализацию оперативной памяти 104 (записав в него модель, спецификацию и выполнив инициализацию формальной проверки модели), включает в работу по своему управляющему выходу модуль формальной проверки модели 105. На шагах от 5 до n происходит переключение вложенных циклов внутри блока формальной проверки модели, где n - количество итераций, необходимое для осуществления полной формальной проверки модели, зависящее от спецификации программы и поведении модели при осуществлении моделирующих итераций. В случае появления на шагах от пяти до n команды 5а на входе интерфейсного распределительного блока, необходимой для принуждения остановки процесса проверки, происходит остановка интерфейсным распределительным блоком по управляющему выходу блока управления, который в этом случае подает досрочный управляющий сигнал блоку обработки результатов проверки 106, что приводит после прочтения последним блоком данных в блоке оперативного хранения данных к появлению на информационном выходе блока обработки результатов проверки сообщения о принудительной остановке процесса проверки модели (команда 5б) и завершению цикла проверки согласованности. В штатном режиме протекания процесса проверки, блок управления после проведения модулем формальной проверки модели (включая итерацию n), по управляющему выходу выдает сигнал о завершении проверки, что проводит к чтению блоком обработки результатов проверки по информационному входу (данные n+1) данных о результатах проверки. Обработав результаты проверки, блок обработки результатов проверки на шаге n+2 (команда n+2) выдает сообщение интерфейсному распределительному блоку для передачи последним на шаге n+3 (команда n+3) этих данных внешнему управляющему вычислительному устройству.