?
A State-based Refinement Technique for Event-B
P. 55–60.
Formal models can be used to describe and reason about the behavior and properties of a given system. In some cases, it is even possible to prove that the system satisfies the given properties. This allows detecting design errors and inconsistencies early and fixing them before starting development. Such models are usually created using stepwise refinement: starting with the simple, abstract model of the system, and then incrementally refining it adding more details at each subsequent level of refinement. Top levels of the model usually describe the high-level design or purpose of the system, while the lower levels are more directly comparable with the implementation code. In this paper, we present a new, alternative refinement technique for Event-B which can simplify the development of complicated models with a large gap between high-level design and implementation.
Language:
English
In book
Los Alamitos: IEEE Communications Society, 2020.
Andrei Akhremenko, Koncha V., Journal of Social Policy Studies 2025 Vol. 23 No. 4 P. 781–794
Due to the heterogeneous composition of modern opposition movements, protesters may have two different types of identity: a narrow one associated with their political group or organization or a widespread identity related to the opposition as a whole. Accordingly, the authorities can use two types of repression: broad, directed against the entire opposition, or targeted, ...
Added: May 13, 2024
Akhremenko A. S., Полис. Политические исследования 2024 № 2 С. 118–134
The influence of Internet communication on “street” protest activity is the focus of this paper. In recent years, there has been some stagnation in this area of research: a shortage of breakthrough works that indicate new research directions or at least significantly strengthen the empirical foundation of already established hypotheses. The paradox is that when ...
Added: March 31, 2024
Bernardinello L., Irina Lomazova, Nesterov R. et al., , in: Transactions on Petri Nets and Other Models of Concurrency XVIVol. 13220: Lecture Notes in Computer Science.: Springer, 2022. P. 1–23.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their ...
Added: March 23, 2022
Akhremenko A. S., Petrov A., , in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020)Vol. 2795.: CEUR Workshop Proceedings, 2020. Ch. 1 P. 1–11.
Over the last 30 years, numerous studies have shown that repression can de-crease, increase, or have some kind of a nonlinear or mixed impact on the intensity of protest. This problem is usually referred to as the “protest-repression nexus” or the “punishment puzzle”, and it is still not resolved. The mathematical and computational model that we present in ...
Added: March 3, 2021
Kuliamin V., Khoroshilov A. V., Medvedev D., , in: Actual Problems of Systems and Software Engineering APSSE 2019 (Invited Papers).: Los Alamitos, Washington, Tokyo: IEEE Computer Society, 2019. P. 131–136.
The paper presents formal security model of Linux distributions provided by Bazealt SPO, which integrates multi-level security (MLS) and mandatory integrity control (MIC) implemented on the base of SELinux framework. The model also includes information flows analysis framework described as an extended Take-Grant model. The main novelty of the model is the integration of MLS ...
Added: October 30, 2020
Bernardinello L., Lomazova I. A., Nesterov R. et al., , in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020)Vol. 2651: CEUR Workshop Proceedings.: CEUR-WS.org, 2020. P. 49–67.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their ...
Added: August 12, 2020
S. S. Akbarov, Journal of Algebra and its Applications 2020 Vol. 19 No. 6 P. 1–28
We prove several properties of kernels and cokernels in the category of augmented involutive
stereotype algebras: 1) this category has kernels and cokernels, 2) the cokernel is preserved under the
passage to the group stereotype algebras, and 3) the notion of cokernel allows to prove that the continuous
envelope Env C*(Z · K) of the group algebra of ...
Added: June 8, 2019
Akbarov S. S., Dissertationes Mathematicae 2016 Vol. 513 P. 1–188
An envelope in a category is a construction that generalizes the operations of “exterior completion”, like completion of a locally convex space, or the Stone–Čech compactification of a topological space, or the universal enveloping algebra of a Lie algebra. Dually, a refinement generalizes the operations of “interior enrichment”, like bornologification (or saturation) of a locally ...
Added: September 23, 2016
Khoroshilov A. V., Petrenko A. K., Девянин П. Н. et al., , in: Abstract State Machines, Alloy, B, TLA, VDM, and Z.: Heidelberg: Springer, 2014. P. 309–313.
The paper presents a work-in-progress on formal verification
of operating system security model, which integrates control of confi dentiality and integrity levels with role-based access control. The main
goal is to formalize completely the security model and to prove its con sistency and conformance to basic correctness requirements concerning
keeping levels of integrity and confidentiality. Additional goal is to per form ...
Added: November 1, 2015
Smeliansky R. L., Chemeritsky E. V., Zakharov V., Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398–406
Software-de ned networking (SDN) is an approach to building computer net- works that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and ow-table updating was de ned in the form of a protocol known ...
Added: September 30, 2015
Andrei Akhremenko, Petrov A., / NRU Higher School of Economics. Series PS "Political Science". 2014. No. WP BRP 16/PS/2014.
The main focus of this paper is the impact of efficiency losses, related to public capital stock, on the prospects of economic growth in democratic and autocratic political environments. We introduce a distinction between two types of efficiency loss: along with the loss of public capital during its accumulation, we take into account the process ...
Added: October 24, 2014
Akhremenko A. S., Petrov A., В кн.: Математическое моделирование и информатика социальных процессов. Сборник трудовВып. 16.: М.: Экон-Информ, 2014. С. 15–20.
В настоящей работе рассматривается динамическая модель, в центре внимания которой находится влияние на эффективность социально-политической системы со стороны уровня налоговой нагрузки и правила распределения бюджетных средств на инвестиции в инфраструктуру и производственный ресурс ...
Added: October 24, 2014
М.: Экон-Информ, 2014.
The articles in this collection are written on the basis of reports made in 2013 at the sociological faculty of Moscow State University M.V. Lomonosova at the annual meeting of the XVI Interdisciplinary Scientific Seminar "Mathematical modeling of social processes" named Hero of Socialist Labor Academician A.A. Samarskogo.
The publication is intended for researchers, teachers, students, ...
Added: October 24, 2014
Efimenko I., Khoroshevsky V. F., В кн.: XIV Национальная конференция по искусственному интеллекту с международным участием КИИ-2014.: Каз.: Российская ассоциация искусственного интеллекта, 2014. С. 118–127.
В работе обсуждаются вопросы создания формальной модели предметной области дорожного картирования на основе анализа лучших практик в данной области. Создание такой модели позволит обобщить опыт построения технологических дорожных карт и обеспечит основу для разработки средств автоматизации формирования и использования дорожных карт. Разработана система онтологий, специфицирующих ключевые информационные объекты сферы дорожного картирования, а также процессные модели лучших ...
Added: October 23, 2014
Akhremenko A. S., Petrov A., В кн.: Метод: московский ежегодник трудов из обществоведческих дисциплинВып. 4.: М.: ИНИОН РАН, 2014. С. 62–82.
The article provides an overview of formal model that demonstrates the connections between institutional investment and social efficiency. The results of a set of computational experiments are described and analyzed. Some problems of mathematical modeling methodology are also discussed in the paper. ...
Added: October 15, 2014
Antonina K. Begicheva, Lomazova I. A., , in: Proceedings of the 8th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2014).: M.: -, 2014. P. 77–82.
Process mining is a new technology, that provides us a variety of methods to discover, monitor and improve real processes by extracting knowledge from event logs. The two most prominent process mining tasks are process discovery and conformance checking. Conformance checking deals with diagnosing and quantifying discrepancies between observed behavior, represented in event logs, and ...
Added: June 2, 2014
Shershakov S., В кн.: Proceedings of the 9th Central & Eastern European Software Engineering Conference in Russia.: NY: ACM, 2013.
Process-aware information systems (PAIS) enable developing models for interaction of processes, monitoring accuracy of their execution and checking if they interact with each other properly. PAIS can generate large data logs that contain the information about the interaction of processes in time. Studying PAIS logs with the purpose of data mining and modeling lies within ...
Added: December 21, 2013