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

Предложена методика верификационной отладки алгоритмов регулирования и вычислительных задач АСУ ТП, заданных функциональными схемами, использующая свойства аппарата LF-функций. Исследованы типичные критерии правильности алгоритмов данного типа. Разработаны схемы извлечения знаний разработчика о правильности алгоритмов различных типов, необходимые для построения и доказательства теорем верификации. Возможности методики верификационной отладки показаны на примерах функциональных схем различных типов.

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

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

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