Статья
Генерация тестовых программ для микропроцессоров на основе спецификаций подсистем памяти
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно-
ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров.
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промыш- ленных микропроцессоров.
Приводятся общие сведения о характеристиках аппаратного обеспечения ЭВМ, рассматриваются основные вопросы организации и функционирования современных ЭВМ и вычислительных систем: история развития, классификация, функциональная и структурная организация ЭВМ, основные архитектуры, принципы функционирования основных подсистем ЭВМ (обрабатывающей, памяти, ввода/вывода, прерываний). Предназначено для студентов специальности 2201 – «Вычислительные машины, комплексы, системы и сети» факультета АВТ дневного отделения. Утверждено Редакционно-издательским советом МГИЭМ в качестве учебного пособия.
This volume contains the papers presented at CS&P 2016, the 25th International Workshop on Concurrency, Specification and Programming, held on September 28 - 30, 2016 in Rostock, Germany. Since the early seventies Warsaw University and Humboldt University have alternately organized an annual workshop - since the early nineties known as CS&P. Over time, it has grown from a bilateral seminar to a well-known meeting attended also by colleagues from many other countries than Poland and Germany. This year marks an anniversary: we celebrate the quarter-centenary edition of CS&P. We do so on the Baltic Sea coast, in one of the oldest universities in the world, the University of Rostock, founded in 1419. The gathering is hosted by Rostock University’s department of computer science, and the editor would like to thank Prof. Karsten Wolf and his local team for their hospitality and great organization. During the three-day meeting, there are 14 sessions in two parallel tracks. Additionally, there is a number of short presentations on current and emerging topics, as well as tool demos and open discussions. This volume contains 26 papers supplementing the presentations, selected from the submissions by the program committee. Following the workshops tradition, we strive to retain an informal working atmosphere. Therefore, the proceedings includes drafts and extended abstracts as well as fully elaborated contributions. The proceedings are published by Humboldt University and CEUR. The editor would like to thank the university’s printing office, the team at CEUR Workshop Proceedings, and EasyChair for their help in producing this publication.
Данное учебное пособие предназначено для студентов первого курса, изучающих английский язык в области информационных технологий по теме 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.
В данной работе рассматривается пятое уравнение Пенлеве, которое имеет 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)