?
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 et al., Proceedings of the Institute for System Programming of the RAS 2023 Vol. 35 No. 3 P. 171–186
Enterprises often provide their services via a family of applications based on various platforms.
Applications in such a family can behave differently. Their development processes can differ as well. Moreover, modern development processes are often complex and sometimes vague. This can lead to bugs, defects, and unwanted discrepancies in applications. In this paper, we show that ...
Added: October 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.
Blockchain technology has developed rapidly over the last few years. A Blockchain network uses the multi-party agreement concept to reach an agreement on the transaction confirmation. As the technology is new, tools and techniques for blockchain verification are still under development. We explore optimization techniques of weighted multi-party agreements with stochastic properties in the current ...
Added: June 16, 2023
ООО «Макс Пресс», 2022.
The book contains the conference abstracts approved by the Program Committee of the joint conference "OSS: from training to development". ...
Added: November 16, 2022
Afanasyev V., Поляков С. А., Бородин А. Е. et al., Труды Института системного программирования РАН 2021 Т. 33 № 6 С. 67–82
The paper describes a static analysis for finding defects and computing metrics for programs written in the Kotlin language. The analysis is implemented in the Svace static analyzer developed at ISP RAS. The paper focuses on the problems we met during implementation, the approaches we used to solve them, and the experimental results for the ...
Added: September 7, 2022
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Sequential reactive systems include programs and devices that work with two streams of
data and convert input streams of data into output streams. Such information processing systems
include controllers, device drivers, computer interpreters. The results of operation of such computing
systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite
transducers are most often ...
Added: January 17, 2022
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification ...
Added: January 17, 2022
Павлова Н. С., Kurdin A., Поляков Д. А., Вестник Московского университета. Серия 6: Экономика 2021 № 1 С. 103–127
The article is based on the research in mobile applications markets. The distribution of market power in these markets depends on the ability of a digital ecosystem’s owner to control the handling of mobile applications inside the ecosystem. The degree of this control is determined by the substitutability of different application stores as necessary facilities ...
Added: July 2, 2021
Gnatenko A., Zakharov V., Системная информатика 2020 Vol. 17 P. 21–32
Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop ...
Added: November 9, 2020
Gnatenko A., Zakharov V., 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 ...
Added: October 17, 2019
Zakharov V., Винарский Е. М., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 257–260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Added: October 17, 2019
Gnatenko A., Zakharov V., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 263–266.
Описаны синтаксис и семантика нового расширения Reg-CTL* темпоральной логики деревьев вычислений CTL*, предназначенного для спецификации и верификации вычислений последовательных реагирующих систем. Поеказано, что задача верификации моделей автоматов-преобразователей относительно выполнимости формул логики CTL* является PSPACE-полной. ...
Added: October 17, 2019
Boris Ulitin, Eduard Babkin, Tatiana Babkina et al., , in: Lecture Notes in Business Information ProcessingIssue 365: Perspectives in Business Informatics Research.: Switzerland: Springer, 2019. P. 59–73.
The article is devoted to the problem of automated formal verification of modeling artifacts during engineering of digital transformations. Automation significantly increases the quality of model transformations since many manual errors are eliminated. However, the formal checking the correctness of such automation remains an open question. One more problem is the dependence of the procedure ...
Added: September 30, 2019
Gostev I. M., М.: Юрайт, 2018.
В настоящее время компьютерные науки стремительно развиваются. Новые версии операционных систем появляются каждые полтора-два года, поэтому было принято решение о включении в данную книгу такого материала, который не будет устаревать. Содержание учебника представляет собой некоторые наиболее общие принципы построения операционных систем, которые были разработаны более 50 лет назад и практически не изменились за прошедшее время. ...
Added: February 13, 2019
Springer, 2018.
This book constitutes the refereed proceedings of the 4th International Conference on Tools and Methods for Program Analysis, TMPA 2017, Moscow, Russia, March 3-4, 2017.
The 12 revised full papers and 5 revised short papers presented together with three abstracts of keynote talks were carefully reviewed and selected from 51 submissions. The papers deal with topics such as ...
Added: November 12, 2018
Kamkin A., М.: МАКС Пресс, 2018.
This textbook is devoted to formal methods for program verification and is based on the lectures given by the author at CMC MSU, DCAM MIPT, and FCS HSE. It describes the basics of such approaches as deductive analysis and model checking. The list of topics includes formal semantics of programming languages (operational and axiomatic semantics), ...
Added: November 2, 2018
Zakharov V., Gnatenko A., , 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.
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite 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 flows of control signals ...
Added: October 26, 2018
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506–524
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between flows of control signals ...
Added: October 26, 2018
Skovoroda A., Gamaunov D., , in: 2017 15th Annual Conference on Privacy, Security and Trust (PST).: IEEE, 2017. P. 243–252.
In this paper we propose a heuristic approach to static analysis of Android applications based on matching suspicious applications with the predefined malware models. Static models are built from Android capabilities and Android Framework API call chains used by the application. All of the analysis steps and model construction are fully automated. Therefore, the method ...
Added: October 12, 2018
Анализ мобильных приложений с использованием моделей привилегий и API-вызовов вредоносных приложений
Gamaunov D., Сковорода А. А., Прикладная дискретная математика 2017 № 36 С. 84–105
In this paper, we propose a heuristic approach to static analysis of Android applications based on matching suspicious applications with the predefined malware models. Static models are built from Android capabilities and Android Framework API call chains used by the application. All of the analysis steps and model construction are fully automated. Therefore, the method can ...
Added: September 13, 2018
Shastitko A., Kurdin A., Управленец 2017 № 4 (68) С. 43–52
The article assesses the policies instituted by producers of operating systems, when they aim to boost sales of applied software integrated into their operating systems. It analyses the policies through the prism of the effects they exert on other participants of the markets for operating systems and applied software. To perform the analysis, the authors ...
Added: August 23, 2018
Gnatenko A., Zakharov V., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303–324
The syntax and semantics of the new temporal logic LP-CTL * designed for the formal specification of the behavior of sequential responsive programs, modeled by automata-transducers (transducers) over semigroups, are developed. An algorithm is developed for verifying the feasibility of the formulas of the proposed temporal logic on models represented by finite transducers working on ...
Added: June 14, 2018
Гнатенко А. Р., Zakharov V., В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды.: МГУ, МАКС Пресс, 2018. С. 131–133.
The expressive power of a new variant of temporal logic LP-CTL * is studied. In this logic, two classes of LP-1-LTL and LP-n-LTL formulas were distinguished and it was shown that the LP-1-LTL fragment more expressive than the known temporal logic of linear time LTL, and the LP-n-LTL fragment has the same expressive possibilities as ...
Added: June 14, 2018