?
Verification and analysis of variable operating systems
Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 189–208.
This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.
L.А. Rezunik, A.I. Perevoznikova, D.V. Eremina и др., Proceedings of the Institute for System Programming of the RAS 2023 Vol. 35 No. 3 P. 171–186
Коммерческие предприятия часто предоставляют свои услуги с помощью семейства приложений, разработанных для работы на различных платформах. Приложения в таком семействе могут вести себя по-разному. Процессы их разработки также могут отличаться. Более того, современные процессы разработки часто сложны, а иногда и не вполне четко определены. Это может приводить к ошибкам, дефектам и нежелательным отличиям в поведении ...
Добавлено: 30 октября 2023 г.
Fedotov I., Anton Khritankov, Barger A., , in: 2022 4th Conference on Blockchain Research and Applications for Innovative Networks and Services, BRAINS 2022.: IEEE, 2022. P. 55–58.
Добавлено: 16 июня 2023 г.
ООО «Макс Пресс», 2022.
В книге собраны тезисы конференции, одобренные Программным комитетом объединённой конференции «СПО: от обучения до разработки». ...
Добавлено: 16 ноября 2022 г.
Афанасьев В. О., Поляков С. А., Бородин А. Е. и др., Труды Института системного программирования РАН 2021 Т. 33 № 6 С. 67–82
В статье описывается статический анализатор для поиска ошибок и анализа метрик и отношений в программах на языке Kotlin. Анализатор был реализован с помощью расширения инструмента Svace, разрабатываемого в ИСП РАН. В статье описываются проблемы, с которыми мы столкнулись в ходе выполнения работы, и предложенные методы их решения, а также экспериментальные результаты полученного анализатора. Инструмент умеет ...
Добавлено: 7 сентября 2022 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Добавлено: 17 января 2022 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Павлова Н. С., Курдин А. А., Поляков Д. А., Вестник Московского университета. Серия 6: Экономика 2021 № 1 С. 103–127
Статья основана на результатах исследования рынков мобильных приложений. Распределение рыночной власти на этих рынках зависит от способности владельца цифровой экосистемы контролировать обращение мобильных приложений внутри своей экосистемы. Степень этого контроля определяется взаимозаменяемостью различных магазинов мобильных приложений как необходимых инструментов для предоставления доступа к мобильным приложениям. Авторы предоставляют основанные на результатах опроса эмпирические оценки такой взаимозаменяемости ...
Добавлено: 2 июля 2021 г.
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663–675
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...
Добавлено: 17 октября 2019 г.
Захаров В. А., Винарский Е. М., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 257–260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Добавлено: 17 октября 2019 г.
Гнатенко А. Р., Захаров В. А., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 263–266.
Описаны синтаксис и семантика нового расширения Reg-CTL* темпоральной логики деревьев вычислений CTL*, предназначенного для спецификации и верификации вычислений последовательных реагирующих систем. Поеказано, что задача верификации моделей автоматов-преобразователей относительно выполнимости формул логики CTL* является PSPACE-полной. ...
Добавлено: 17 октября 2019 г.
Boris Ulitin, Eduard Babkin, Tatiana Babkina и др., , in: Lecture Notes in Business Information ProcessingIssue 365: Perspectives in Business Informatics Research.: Switzerland: Springer, 2019. P. 59–73.
Добавлено: 30 сентября 2019 г.
Гостев И. М., М.: Юрайт, 2018.
В настоящее время компьютерные науки стремительно развиваются. Новые версии операционных систем появляются каждые полтора-два года, поэтому было принято решение о включении в данную книгу такого материала, который не будет устаревать. Содержание учебника представляет собой некоторые наиболее общие принципы построения операционных систем, которые были разработаны более 50 лет назад и практически не изменились за прошедшее время. ...
Добавлено: 13 февраля 2019 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Захаров В. А., Гнатенко А. Р., , in: Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018.: Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29–36.
Добавлено: 26 октября 2018 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506–524
О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых ...
Добавлено: 26 октября 2018 г.
Skovoroda A., Гамаюнов Д. Ю., , in: 2017 15th Annual Conference on Privacy, Security and Trust (PST).: IEEE, 2017. P. 243–252.
Добавлено: 12 октября 2018 г.
Анализ мобильных приложений с использованием моделей привилегий и API-вызовов вредоносных приложений
Гамаюнов Д. Ю., Сковорода А. А., Прикладная дискретная математика 2017 № 36 С. 84–105
Предложен метод автоматической классификации мобильных приложений на основе статического анализа и сопоставления моделей, полученных по его результатам, с моделями ранее известных вредоносных приложений. Модели основаны на привилегиях и API-вызовах, используемых в приложении. Все шаги анализа, а также построение моделей полностью автоматизированы. Таким образом, метод адаптирован для автоматизированного использования магазинами мобильных приложений или другими заинтересованными организациями. ...
Добавлено: 13 сентября 2018 г.
Шаститко А. Е., Курдин А. А., Управленец 2017 № 4 (68) С. 43–52
Статья посвящена оценке влияния политики производителей операционных систем, развивающих продажи прикладного программного обеспечения в составе операционной системы, на положение иных участников рынков операционных систем и прикладного программного обеспечения. Анализ проводится на примере рынков антивирусного программного обеспечения в связи с выпуском корпорацией Microsoft собственной встроенной антивирусной программы Defender при одновременном ужесточении политики Microsoft в отношении других ...
Добавлено: 23 августа 2018 г.
Гнатенко А. Р., Захаров В. А., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303–324
Добавлено: 14 июня 2018 г.
Гнатенко А. Р., Захаров В. А., В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды.: МГУ, МАКС Пресс, 2018. С. 131–133.
Проведено сравнение выразительных возможностей темпоральной логики LP-CTL*. В этой логике были выделены два класса формул (фрагмента) LP-1-LTL и LP-n-LTL и показано, что фрагмент LP-1-LTL превосходит по выразительным возможностям известную темпоральную логику линейного времени LTL, а фрагмент LP-n-LTL имеет такие же выразительные возможности, что и монадическая логика второго порядка с одной функцией следования S1S. ...
Добавлено: 14 июня 2018 г.