TMPA-2013: программа

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

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

Современные методы обеспечения высокого качества ПО включают целый арсенал средств, методик и подходов. Хотя основным методом здесь все еще остаются тестирование и отладка программ, в последнее время все более широкое применение получает верификация – формальное доказательство выполнения на формальной модели программной системы формально определенных требований к ее поведению. Прорывным направлением в области формальной верификации стал метод Model checking (проверка модели.

Метод Model checking может быть использован для программных и аппаратных систем, которые представляются модель переходов с конечным числом состояний, поэтому главной проблемой этого метода является «state explosion problem», состоящая в экспоненциальном росте числа состояний системы параллельных программ при увеличении числа взаимодействующих компонент. Разработка «символьных» алгоритмов, основанных на экономных методах представления конечных структур данных, позволило во многом снизить чувствительность этого метода к проблеме “взрыва” числа состояний и существенно увеличить эффективность этого метода верификации. «Символьные» методы верификации были с успехом использованы во многих практических разработках реальных программных систем. Сегодня эта техника применяется как этап технологии во многих крупных фирмах, занимающихся разработкой встроенных систем для критических применений.

Область Model checking остается «горячей» областью информатики, здесь продолжаются интенсивные исследования, возможности этого подхода постоянно расширяются. Недавно группой ведущих ученых в области применения формальных методов в разработке ПО был объявлен амбициозный международный исследовательский проект «Verified Software Initiative», целью которого является доведение теоретических основ, инструментария и элементов технологии верификации до такого состояния, при котором они позволят строить программные системы, вовсе не содержащие ошибок.

Аннотация. В последние 10 лет практически повсеместно аналоговые контуры управления вытесняются цифровыми. В настоящее время ведутся работы по созданию цифровых систем управления критическими системами: «интеллектуальные подстанции» в электроэнергетике, «интегрированная модульная авионика» в авиации, «интеллектуальные фабрики» в промышленности и т.д.

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

Аннотация. В последние несколько лет активное развитие получили программно-конфигурируемые сети (ПКС) - особый вид компьютерных сетей, в которых все коммутирующие устройства имеют централизованное управление. В статье исследуются задачи формального описания и верификации ПКС. Для описания ПКС используется библиотека элементов UML в редакторе диаграмм Dia. Для верификации ПКС используется программно-инструментальное средство UPPAAL. Основной результат исследований – разработка транслятора, позволяющего по диаграмме сети получить ее модель для верификации в виде сети конечных временных автоматов. Корректность алгоритма трансляции строго обоснована. Проведен ряд экспериментов, которые показывают применимость предложенного метода верификации для проверки свойств поведения ПКС, специфицированных посредством формул темпоральной логики реального времени.

Аннотация. Описывается подход к программированию логических контроллеров, состоящих в формировании программной LTL-спецификации, последующей ее проверке на корректность средством верификации Cadence SMV и трансляции в код на языке ST.

Аннотация. Статья представляет подход к разработке средств дедуктивной верификации программ. Основой подхода является предметно-ориентированный язык для данной предметной области. Сформулированы требования к такому языку и дано обоснование использования языка спецификации предметно-ориентированных систем переходов Atoment в качестве возможного кандидата. Особенности применения подхода и принципы, на которых он основан, проиллюстрированы на простых примерах. На базе подхода предполагается создать технологию разработки средств дедуктивной верификации программ.

Аннотация. В данной статье рассмотрен комплексный подход к разработке и верификации распределенных автоматных программ, в которых иерархические автоматы могут реализовываться в разных потоках и взаимодействовать друг с другом. Предложен интерактивный подход к верификации распределенных автоматных программ при помощи инструмента Spin, который включает в себя автоматическое построение модели на языке Promela, приведение LTL-формулы в формат, определяемый инструментом Spin и построение контрпримера в терминах автоматов. На основе этого подхода создано инструментальное средство Stater, позволяющее создавать распределенную систему конечных автоматов, генерировать на ее основе программный код на целевых языках программирования и верифицировать ее при помощи верификатора Spin. Автоматы могут быть созданы в инструменте Stater, а также импортированы из Stateflow.