БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

НАУЧНО-ПРАКТИЧЕСКИЕ КОНФЕРЕНЦИИ

<< ГЛАВНАЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ

загрузка...

Pages:     | 1 |   ...   | 13 | 14 || 16 | 17 |   ...   | 28 |

«ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ И СИСТЕМЫ Труды Третьей международной научной конференции Банное, Россия, 26 февраля — 2 марта 2014 года Научное электронное издание Челябинск ...»

-- [ Страница 15 ] --

преобразования документов, выполненных в бумаж- Использование САПР в автономном режиме и при ной форме, в электронную форму [1. С. 3]. Вводятся совместной работе с PDM-системой имеют отличия новые виды конструкторских документов: электрон- в методике построения моделей сборочных единиц, ная модель детали, электронная модель сборочной в реквизитной информации моделей, в справочниединицы, электронная структура изделия [2. С. 1–2]. ках стандартных изделий и материалов, в настройке Соответственно, в качестве ЭКД будем рассматри- САПР. Главными требованиями при совместном исвать перечисленные виды документов и двумерные пользовании САПР и PDM-системы являются разрачертежи деталей и сборочных единиц, выполненные ботка и обязательное выполнение правил работы в Перечислим основные задачи, которые с помощью Основным ЭКД является электронная структура ЭКД решаются эффективнее, чем с использовани- изделия (ЭСИ). ЭСИ является обобщающим докуем документации в бумажной форме: проработка ментом, консолидирующим технические данные об конструкции изделия, проведение инженерных рас- изделии [4. С. 2]. В PDM-системе Windchill для сочетов, создание управляющих программ для обо- здания ЭСИ имеются следующие элементы: объекты рудования с числовым программным управлением, и иерархические связи между ними;

атрибуты объекпроектирование технологической оснастки, создание тов, представляющие реквизитную информацию;

моиллюстраций для текстовой документации. Давно дели и чертежи деталей и сборочных единиц;

связи, уже стала анахронизмом идея автоматизированных определенных типов, между объектами и соответстрабочих мест, соединенных сетевым кабелем, а по вующими моделями и чертежами. Методика испольсути, — информационно и организационно автоном- зования перечисленных элементов и других функциных [3. С. 48]. Разработка ЭКД должна проводиться ональных возможностей PDM-системы Windchill и в среде системы управления инженерными данными САПР Creo Parametric для создания ЭКД зависит от об изделии (PDM-система). Это позволит расширить потребностей и возможностей предприятия, имеюД. Б. Козырев, Е. М. Абакумов Вопросы создания электронной конструкторской документации...

щихся в эксплуатации информационных систем, осо- Параметр «Обозначение_документа» состоит из пабенностей конструкций изделий. Далее представлена раметров «Обозначение» и «Постфикс_модели».

методика, принятая в ФГУП «ВНИИА». Значением параметра «Обозначение» является дециОсновными объектами PDM-системы Windchill, мальное обозначение детали (сборочной единицы).

формирующими состав изделия, являются «части». Параметр «Постфикс_модели» является аналогом «Части», как правило, представляют конкретные де- общепринятого понятия «Код документа», но имеет тали, сборочные единицы или сборочные материалы более широкий смысл, так как присваивается всем и имеют соответствующие реквизиты. Чтобы состав моделям, которые могут и не иметь соответствующеизделия преобразовать в ЭСИ, с «частями» связыва- го документа. Например, для модели детали, парают CAD-документы — модели и чертежи деталей, метр имеет значение «МД», для габаритной модели, созданные в САПР Creo Parametric. На рис. 1 пред- описывающей внешнее представление изделия — «Части», иерархические связи между ними и связи с CAD-документами создаются в автоматизированном режиме на основе модели сборочной единицы, с возможностью выбора необходимости создания «части» для каждого CAD-документа и типа связи между «частью» и CAD-документом. К «частям»

ссылками привязываются соответствующие им дополнительные документы, разработанные в другом программном обеспечении, например текстовые документы. Для «частей» создают набор атрибутов, который зависит от того какому разделу спецификации изделия соответствует «часть». Значения атрибутов передаются в «части» из соответствующих параметров моделей.

При создании в САПР Creo Parametric моделей и Рис. 2. Пример «части», связанной с двумя моделями чертежей, удовлетворяющим требованиям к ЭКД, необходимо учитывать, что на основе модели сбо- Другой особенностью изделий является наличие рочной единицы будет создаваться ЭСИ, и все мо- в конструкции моточных изделий, тонкослойных дели будут использоваться для проведения техноло- сборочных единиц и сложных заделок проводов в гической подготовки производства. Таким образом, разъемах. Такие элементы конструкции создавать в происходит все большее слияние и взаимопроник- виде моделей сборочных единиц нецелесообразно.

новение собственно конструкторского и технологи- Поэтому они заменяются габаритными моделями, а в ческого этапов проектирования [5. С. 357]. Также качестве основного документа используется чертеж.

необходимо провести настройку конфигурационных Таким образом, «часть», сопоставленная моточному файлов САПР Creo Parametric, создать шаблоны для изделию, имеет связь «Владелец» с чертежом и связь всех типов CAD-документов: моделей деталей и «Изображение» с габаритной моделью.

сборочных единиц, габаритных моделей, моделей Создание моделей сборочных единиц и ЭСИ возстандартных и прочих изделий, моделей сборочного можно только с использованием справочников моделей материала, чертежей всех форматов. При совместном стандартных изделий и материалов, которые создаются использовании рассматриваемых систем, уникаль- по специальным шаблонам на основе действующих обность каждого CAD-документа обеспечивается ис- щесистемных справочников ФГУП «ВНИИА».

пользованием параметра «Обозначение_документа» Спецификация является основным конструктори соответствующим его значению именем файла. ским документом при использовании документации в бумажной форме. При использовании ЭКД и PDM- шагами с поэтапным решением вопросов. При этом, системы спецификация уже не является необходи- использование ЭКД должно вписаться в имеющуюся мым документом, а всего лишь отражает ЭСИ и по- информационную инфраструктуру и во время перелучается в виде отчета из ЭСИ. Для этого разработан ходного периода должна использоваться совместно с дополнительный модуль к PDM-системе. документацией в бумажной форме. Важнейшим орПосле создания ЭСИ проводится процесс утвер- ганизационно-техническим вопросом является выраждения ЭКД в соответствии с разработанным в PDM- ботка методических рекомендаций и утверждение месистеме маршрутом, который позволяет привлекать тодики создания ЭКД с учетом этого обстоятельства.

необходимых специалистов. Специалисты используют визуализатор с функцией «красного карандаша», позволяющий не использовать лицензии САПР. В PDM-системе Windchill, как и в других PDM-системах, отсутствует полноценный модуль управления электронным архивом технической документации.

Поэтому для регистрации и обработки ЭКД была разработана собственная система. Утвержденная и зарегистрированная ЭСИ является источником информации для других информационных систем предприятия, в которые она попадает через разработанный модуль передачи информации.

Создание ЭКД имеет технические, методические, информационные и организационные вопросы. Внедрение ЭКД на предприятии возможно постепенными Д. Б. Козырев, Е. М. Абакумов Вопросы создания электронной конструкторской документации...

ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ АЛГОРИТМОВ

С ПОМОЩЬЮ ТЕХНИКИ ПРОВЕРКИ МОДЕЛЕЙ...

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

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

Подробная классификация методик верификации представлена в работе [1]. Особое положение среди описанных в этой работе подходов занимают формальные методы, связанные с исследованием модели алгоритма (реализация) и требований к нему (спецификация).

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

2].

Верификация на основе метода обладающих высокой степенью параллелизма.

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

го анализа (automated theorem proving), техника про- 1. Сформировать модель (структуру Крипке), эквиверки эквивалентности (formal equivalence checking) и валентную верифицируемому алгоритму.

техника проверки моделей (model checking) [2]. Наи- 2. Сформировать спецификацию (выражение LTL), более трудоемким является последнее из них. Однако отражающую требования к алгоритму.

в связи с постоянно возрастающей вычислительной 3. Посредством методов логического вывода выполмощностью современных высокопроизводительных нить сопоставление модели и спецификации. В случае систем методы верификации на основе model checking успешного завершения вывода считать алгоритм корявляются наиболее перспективными, т. к. могут быть ректным, в противном случае — некорректным.

Техника проверки моделей может быть охарактери- фикации параллельных алгоритмов на основе техники зована как строгая методология, включающая три ком- проверки моделей и аппарата логического вывода.

Рис. 1. Структура комплекса для формальной верификации параллельных алгоритмов для сопоставления реализации и спецификации ния. Структурная схема МЛВ изображена на рис. 2.

Для осуществления проверки логическими мето- Представленная на рисунке структура МЛВ опредедами соответствия модели алгоритма предъявляемым ляется шагами предлагаемого метода вывода. Отдельно требованиям необходимо сформировать базу знаний, стоит отметить блоки диспетчеризации и предобраотражающую взаимосвязь между состояниями объекта ботки. Диспетчер позволяет изменять стратегию разисследования и его существенными свойствами. Дан- мещения вновь получаемых задач в очереди. Данное ное действие может быть выполнено путем применения решение делает возможным использование различных представленного в работе [3] способа. Важной харак- эвристик, которые в некоторых случаях способны притеристикой получаемой базы знаний является полнота, вести к скорейшему получению результата. Блок предопозволяющая решить проблему логического отрицания. бработки выполняет частичную фильтрацию данных, Для сопоставления модели и требований предлага- отбрасывая факты, которые не могут повлиять на текуется использовать специально разработанный метод щий шаг вывода. С помощью данного механизма удалогического вывода делением дизъюнктов на основе ется сократить время, необходимое для решения одной определяющего элемента (МДДОЭ), который бази- задачи, на несколько порядков.

руется на обобщенном методе деления дизъюнктов Остается добавить, что в случае необходимости в логике предикатов первого порядка [4]. Наиболее вместо МДДОЭ может быть использован любой изважными преимуществами МДДОЭ являются следу- вестный метод вывода, подробный обзор которых – отдельные шаги вывода при получении множества новых выводимых дизъюнктов могут выполняться – связь по данным между шагами вывода мини- ретический базис, позволяющий выполнять верифив ходе вывода не требуется модификация базы проверки моделей с применением теории логическознаний (не происходит порождения новых фактов). го вывода.

Таким образом, при реализации МДДОЭ на систе- Кроме того, ведутся работы по созданию специмах с общей памятью возможно получение ускоре- ализированного аппаратного ускорителя на базе ния, близкого к числу задействованных процессоров. ПЛИС для выполнения операции унификации.

Кроме того, аналитические оценки показывают, что Предлагаемый в работе метод формальной вериметод позволит получить значительное ускорение и фикации с помощью математического аппарата тена системах с разделяемой памятью. ории логического вывода позволяет в несколько раз Одним из наиболее важных элементов описывае- сократить время, необходимое для сопоставления мого подхода к верификации является машина логического вывода (МЛВ), функционирующая на основе В. Ю. Мельцов, Г. А. Чистяков Формальная верификация алгоритмов с помощью техники проверки моделей...

Данный подход будет использован в программном 3. Мельцов, В. Ю. Формирование базы знаний на комплексе верификации программного обеспечения основе структуры Крипке и формул темпоральной для многопроцессорных и распределенных супер- логики / В. Ю. Мельцов, Г. А. Чистяков // Фундамент.

1. Кулямин, В. В. Методы верификации программ- тротехн. ун-т, 1998.

ного обеспечения. М. : Ин-т системного программи- 5. Вагин, В. Н. Достоверный и правдоподобный 2. Карпов, Ю. Г. Model Checking. Верификация па- Е. Ю. Головина, М. В. Загорянская и др. М. :

раллельных и распределенных программных систем. ФизМатЛит, 2008.

СПб. : БХВ-Петербург, 2009.

ОБЗОР ТЕХНОЛОГИИ BIG DATA

Приводятся понятие Big data. Рассматриваются характеристики Big Data, а так же основные подходы, технологии и методы, позволяющие обрабатывать большие данные.

Big Data (большие данные) — представляет собой Основным преимуществом распределенных сисочень большое количество информации. Такой объем тем является способность неограниченного увеличеинформации становится крайне сложно обработать ния производительности путем линейного масштаобычными программными и аппаратными средства- бирования. Поскольку кластер состоит из большого ми. При этом большая часть обрабатываемых данных количества узлов, и система автоматически перерарегулярно обновляется и представлена в формате, спределяет хранящиеся на них данные, при выводе из плохо соответствующему традиционному структури- строя отдельно взятой или нескольких машин, риски рованному формату БД. Соответственно, возникает потерять какую-либо информацию сведены к мининеобходимость применения новых технологий и ме- муму, тем самым обеспечивая надежность системы.

тодов быстрой обработки таких данных. Таким обра- К тому же высокопроизводительный кластер может зом, термин Big data, включает следующие аспекты: быть реализован на low-end машинах, а значит, его большие объемы регулярно обновляемой информа- стоимость будет существенно ниже, чем стоимость ции, ее разнообразие, необходимость быстрой обра- аналогичного по мощности сервера [4].

ботки, а так же сами подходы, технологии и методы, Необходимо отметить и такой подход работы с Big призванные решать данные задачи [1;

2]. Data как NoSQL базы данных, которые стали активно Одним из таких подходов является система рас- развиваться в виду того, что обработка больших объпределенных вычислений, которая, в свою очередь, емов данных с использованием традиционно попуможет реализовываться различными способами, на- лярных реляционных БД становится все более сложпример, популярной моделью MapReduce, разрабо- ной и ресурсоемкой задачей. Термин NoSQL (not only танной компанией Google. MapReduce представляет SQL) стал общим и не обозначает конкретную техсобой обработку данных, которые разделяются на нологию или продукт. В методологической основе большое количество элементарных заданий, выпол- NoSQL БД лежит принцип теоремы CAP, гласящий, няемых на различных узлах кластера и, в конечном что в распределенной системе невозможно одновреитоге, сводимых в единый результат. Эта модель по- менно обеспечить согласованность данных, доступзволяет обработать несколько петабайт данных. На ность и устойчивость к расщеплению на изолированрисунке показан принцип работы MapReduce [3]. ные части. В результате, NoSQL-системы жертвуют В числе существующих реализаций этой модели согласованностью данных ради достижения высокой можно выделить проект Hadoop, который включает доступности и устойчивости к разделению данных в себя набор утилит и библиотек, а так же каркас для [5;

6]. Зачастую первоочередной задачей NoSQL БД разработки и выполнения распределенных программ, является быстрый поиск небольшого объема инфорработающих на кластерах из сотен узлов. Hadoop ис- мации [7].



Pages:     | 1 |   ...   | 13 | 14 || 16 | 17 |   ...   | 28 |
 


Похожие материалы:

«МАТЕРИАЛЫ ВОСЬМОЙ НАУЧНО-ПРАКТИЧЕСКОЙ КОНФЕРЕНЦИИ Перспективные системы и задачи управления Таганрог 2013 Конференция “Перспективные системы и задачи управления” УДК 681.51 Материалы Восьмой Всероссийской научно-практической конференции Перспективные системы и задачи управления. – Таганрог: Изд-во ТТИ ЮФУ, 2013. – 378 с. Издание осуществлено при поддержке Российского фонда фундаментальных исследований, грант № 13-08-06015. ОРГАНИЗАТОРЫ Министерство обороны РФ; Министерство внутренних дел РФ; ...»

«3 Генеральный секретариат IRU 14 Организации-партнеры IRU 18 Автомобильный транспорт 19 Приоритетные задачи IRU: устойчивое развитие 20 Безопасность дорожного движения 20 Инновации 21 Академия IRU 26 Система стимулирования 30 Инфраструктура 32 Приоритетные задачи IRU: содействие развитию торговли, туризма и автотранспорта 34 Общий контекст и вопросы, связанные с торговлей 34 Содействие автомобильным перевозкам и вопросы безопасности 38 4-я Конференция IRU по автотранспортным перевозкам ...»

«08 основные операции 09 Агентство по распределению номеров Интернета 10 Группа DNS 10 Информационные технологии 10 Группа обеспечения безопасности 12 инициативы 13 Новые gTLD 13 Обзор Утверждения обязательств 15 Глобальное сотрудничество 15 Многоязычные доменные имена 16 Оценка строки IDN ccTLD 17 Программа грантов 17 Общественные конференции ICANN 18 Участие и привлечение 18 Программа для новичков ФотограФия на обложкЕ 19 консультативные советы и вспомогательные организации Члены совета ...»

«ИНТЕРВЬЮ с. 6–7 Дик Ватика: Расизм сдерживает развитие СОЦИАЛЬНЫЕ ПРЕОБРАЗОВАНИЯ с. 26 Новый этап в программе ЮНЕСКО МОСТ ДОСЬЕ с. 12–23 Молодежь создает завтрашний мир www.unesco.org/shs/views 2 Июнь/сентябрь 2007 ОТ РЕДАКЦИИ 17 Повышение роли молодежи – путь к устойчивому развитию Жить и видеть ту зарю – блаженство, но быть молодым – это ...»






 
© 2013 www.kon.libed.ru - «Бесплатная библиотека научно-практических конференций»