Статья
Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ — программ на языке ассемблера, создающих разнообразные ситуации (исключения, блокировки конвейера, неверные предсказания переходов, вытеснения данных из кэш-памяти и т.п.). В статье описываются требования, предъявляемые к промышленным генераторам тестовых программ, и представляется генератор для микропроцессоров архитектуры ARMv8, разработанный с использованием инструмента MicroTESK (Microprocessor TEsting and Specification Kit). Генератор поддерживает подмножество команд, характерное для мобильных приложений (около 400 команд) и состоит из двух основных частей: (1) архитектурно независимого ядра и (2) формальной спецификации ARMv8 (точнее, модели, автоматически построенной по формальным спецификациям). При такой организации процесс разработки генератора тестовых программ состоит преимущественно в создании формальных спецификаций, что экономит усилия за счет повторного использования архитектурно независимых компонентов. Архитектура описывается на языках nML и mmuSL: первый язык позволяет описывать регистры микропроцессора, синтаксис и семантику команд; второй — устройство подсистемы памяти (адресные пространства, разного рода буферы и таблицы, алгоритмы трансляции адресов и т.п.). В статье приводятся характеристики разработанного генератора и делается сравнение с существующими аналогами.
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промыш- ленных микропроцессоров.
Монография представляет собой результат исследования проблемы повышения производительности работы программиста в рыночных условиях. Для рыночных условий характерно, что разрабатываемые программы должны представлять собой пусть не лучший, но работающий продукт, соответствующий определённым потребностям рынка. Такие программы могут быть созданы за счёт комплексирования программных средств, то есть за счёт сборки программных средств из существующих программ, часто разработанных на разных алгоритмических языках и не имеющих исходных модулей. Книга может быть полезна бакалаврам, магистрам и аспирантам, обучающимся по специальностям «бизнес-информатика» и «программная инженерия».
В настоящих указаниях приводится описание одной из особенностей организации работы процессоров на уровне микроархитектуры – способа выполнения машинных команд:
• последовательного (при отсутствии конвейеров), • при наличии одного конвейера, • при наличии нескольких конвейеров.Методические указания содержат достаточное число вариантов заданий на курсовую работу для студентов и вопросы для самопроверки. Утверждено Редакционно-издательским советом Московского государственного института электроники и математики в качестве учебного пособия.
Данное учебное пособие предназначено для студентов первого курса, изучающих английский язык в области информационных технологий по теме Hardware. Цель курса научить студентов работать со специальной базой научно-технических данных в названной области.
Представленный материал состоит из 5 разделов, полностью охватывающих указанное направление:
Different Types of Computers Computer Basics Input Devices Output Devices Secondary Storage DevicesПрактика преподавания настоящего аспекта показала целесообразность лексической направленности упражнений и закрепляющего материала. Учебные задания должны способствовать усвоению специальных понятий и терминов в области информационных технологий.
В первом, третьем, четвертом и пятом разделах представлены задания, позволяющие развивать навыки учащихся давать собственную оценку полученной информации. Каждый урок этих разделов включает: тексты-опоры; англо-русский глоссарий; определения базовых терминов; упражнения, закрепляющие понимание терминологии; лексические упражнения, развивающие устную речь. Второй раздел представляет собой изложение структурной схемы персонального компьютера, поэтому упор в этом разделе делается на усвоение специальных терминов и перевод.
Специфика преподавания данного аспекта состоит в необходимости постоянного обновления материала. Тексты-опоры, содержащие всю необходимую терминологию, дополняются материалами сайтов ИТ и, прежде всего, сайтов выставок CES и CeBit. Представляется целесообразным предлагать студентам самостоятельно находить необходимый материал, развивая тем самым навыки поиска и аннотирования информации. На занятиях предполагается вести обсуждение тем с опорой на текст пособия и знакомый учащимся лексико-грамматический материал. Обсуждения носят информационно-познавательный характер.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
Журналы событий, сохраняемые современными информационными и техническими системами, как правило, содержат достаточно данных для автоматизированного восстановления моделей соответствующих процессов. Разработано множество алгоритмов для построения моделей процессов, проверки соответствия фактического поведения системы модельному, сравнения моделей процессов, и т.д. Однако возможность быстрого анализа выбираемых пользователями частей журнала до сих пор не нашла полноценной реализации. В статье описан метод многомерного хранения журналов событий для извлечения и анализа процессов, основанный на подходе ROLAP. Результатом анализа журнала является направленный невзвешенный граф, представляющий собою сумму возможных последовательностей событий, упорядоченных по вероятности их возникновения с учетом заданных условий. Разработанный инструмент позволяет выполнять совместный анализ моделей подпроцессов, восстановленных из частей журнала путем задания критериев отбора событий и требуемого уровня детализации модели.
В монографии приведены результаты исследования, посвященного управлению жизненным циклом информационных систем, а также анализу стандартов, сводов знаний и корпоративных методик, использующихся в ИТ-проектах. Приведены характеристики фаз ЖЦИС из практики управления ИТ-проектами, а также практические рекомендации по управлению такими проектами. Книга предназначена для научных работников, сотрудников научно- технических предприятий и работников государственных органов управлений, а также студентов, аспирантов, слушателей бизнес-школ повышения квалификации и переподготовки кадров. Книга содержит практические рекомендации для руководителей ИТ-проектов, а также сотрудников компаний, занимающихся проектной деятельностью в области ИТ-проектов.
The geographic information system (GIS) is based on the first and only Russian Imperial Census of 1897 and the First All-Union Census of the Soviet Union of 1926. The GIS features vector data (shapefiles) of allprovinces of the two states. For the 1897 census, there is information about linguistic, religious, and social estate groups. The part based on the 1926 census features nationality. Both shapefiles include information on gender, rural and urban population. The GIS allows for producing any necessary maps for individual studies of the period which require the administrative boundaries and demographic information.
В данной работе рассматривается пятое уравнение Пенлеве, которое имеет 4 комплексных параметра. Методами степенной геометрии ищутся асимптотические разложения его решений в окрестности его неособой точки z=z0, z0≠0, z0≠∞, при любых значениях параметров уравнения. Показано, что имеется ровно 10 семейств разложений решений уравнения. Все они - по целым степеням локальной переменной z - z0. Из них одно новое; у него произвольный коэффициент при четвертой степени локальной переменной. Одно из семейств однопараметрическое, остальные - двухпараметрические. Доказано, что все разложения сходятся в окрестности (а являющиеся полюсами - в проколотой окрестности) точки z=z0.
В данной работе рассматривается пятое уравнение Пенлеве, которое имеет 4 комплексных параметра α, β, γ, δ. Методами степенной геометрии ищутся асимптотические разложения его решений при x → ∞. При α≠0 найдено 10 степенных разложений с двумя экспоненциальными добавками каждое. Шесть из них - по целым степеням x (они были известны), и четыре по полуцелым (они новые). При α=0 найдено 4 однопараметрических семейства экспоненциальных асимптотик y(x) и 3 однопараметрических семейства сложных разложений x=x(y). Все экспоненциальные добавки, экспоненциальные асимптотики и сложные разложения найдены впервые. Также уточнена техника вычисления экспоненциальных добавок.
В данной работе рассматривается пятое уравнение Пенлеве. Методами степенной геометрии ищутся асимптотические разложения его решений при x → 0. Получено 27 семейств разложений решений уравнения. 19 из них получены из разложений решений шестого уравнения Пенлеве. Среди остальных 8 семейств одно было известно раньше, ещё одно может быть получено из разложения решения третьего уравнения Пенлеве. Новыми являются 3 семейства полуэкзотических разложений, 2 семейства сложных разложений и семейство степенно-логарифмических разложений.
Электронное издание является сборником материалов международной научно-практической конференции "Теория активных систем" (ТАС-2014)