Verification, Model Checking, and Abstract Interpretation. 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings
Cham : Springer, 2016.
Bouajjani A., Monniaux D.
This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017. The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.
, , , Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398-406
Software-dened 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 dened in the form of a protocol known ...
Added: September 30, 2015
, , , in : Modern Stochastics and Applications. Vol. Springer, Optimization and Its Applications.: Springer, 2014. P. 159-174.
For degenerate Hybrid Stochastic Systems with full Dependence of all components exponential convergence to the stationary regime has been established. ...
Added: October 18, 2014
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени
, , Моделирование и анализ информационных систем 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
Application and Theory of Petri Nets and Concurrency. 35th International Conference, PETRI NETS 2014, Tunis, Tunisia, June 23-27, 2014, Proceedings
Berlin : Springer, 2014
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 ...
Added: July 3, 2014
, , 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
, , Programming and Computer Software 2015 Vol. 41 No. 4 P. 197-207
The paper presents a target analyzable language used for verification of real world production GNU C programs (Linux kernel modules). The language represents an extension of the existing intermediate language used by the Jessie plugin for the Frama C static analysis framework. Compared to the original Jessie, the extension is fully compatible with the C semantics of arrays, ...
Added: October 30, 2015
, , 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
, , , , in : 2016 International Siberian Conference on Control and Communications (SIBCON). Proceedings. : M. : HSE, 2016.
This paper proposes an approach to k-bounded Petri nets behavioral equivalence checking using the model checking method and mainstream verifier nuSMV. For the comparison of behavior of two nets, an add-in net is introduced which performs a supervisory control of these two nets. The approach uses an implicit word-to-word comparison of labeled Petri net languages ...
Added: September 28, 2016
, , В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 204-206.
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя ...
Added: October 13, 2016
, , Вестник Пермского университета. Серия: Экономика 2013 № 1(16) С. 6-11
Dynamic models under consideration cover a wide class of models in mathematical Economics and Ecology taking into account some aftereffects and including equations with both continuous and discrete times. Control problems are considered in a general case when the aimes of control are given by a system of linear functionals with an arbitrary number of ...
Added: October 15, 2013
Berlin : Springer, 2012
This volume constitutes the refereed proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science, MFCS 2012, held in Bratislava, Slovakia, in August 2012. The 63 revised full papers presented together with 8 invited talks were carefully reviewed and selected from 162 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms ...
Added: October 30, 2013
, Вестник Тамбовского университета. Серия: Естественные и технические науки 2013 Т. 18 № 5-2 С. 2735-2737
A continuous-discrete system of functional-differential equations is considered. The main feature of the system under consideration is the presence of both continuous time and discrete time in the state variables and constant delay. The problem of control in the case of only discrete control with aftereffect is formulated. Necessary and sufficient conditions for the solvability ...
Added: October 25, 2013
, , Вестник Тамбовского университета. Серия: Естественные и технические науки 2011 Vol. 16 No. 4 P. 1211-1213
For a functional differential system with continuous and discrete times, the problem of control with respect to an on-target vector-functional is considered. Conditions for the solvability of the problem are obtained. ...
Added: November 14, 2012
, , В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 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
, , Приборы и системы. Управление, контроль, диагностика 2018 № 1 С. 25-33
In this paper author suggests a new hybrid decision support system for operation with a class of semistructured tasks with underdetermined variables. Author defined the general tasks of prediction and estimation for a class of semistructured tasks. Use of interval neural networks and genetic algorithms for such tasks is justified. Author developed the algorithm to ...
Added: February 9, 2018
, , В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 257-260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Added: October 17, 2019
, , 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
, , , in : Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer Science. Vol. 10742.: Springer, 2018. P. 256-275.
Several previous evaluations of memory models for SMT-based deductive verification tools have shown that the choice of memory model may significantly affect both the number of automatically discharged verification conditions and the capabilities of the verification tool. One of the most efficient memory models for deductive verification of low-level C code is based on region ...
Added: February 12, 2018
, , 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
, Oxford : Elsevier, 2019
A Relaxation Based Approach to Optimal Control of Hybrid and Switched Systems proposes a unified approach to effective and numerically tractable relaxation schemes for optimal control problems of hybrid and switched systems. The book gives an overview of the existing (conventional and newly developed) relaxation techniques associated with the conventional systems described by ordinary differential equations. ...
Added: October 30, 2021
Application and Theory of Petri Nets and Concurrency. 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25–30, 2017, Proceedings
Switzerland : Springer, 2017
This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017. The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, ...
Added: May 6, 2017
, , , in : Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016. Vol. 1698.: Humboldt-Universität zu Berlin, 2016. P. 233-244.
By sequential reactive system we mean a program which operates in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data a program performs a sequence of actions (response) and displays the current result. Such programs usually arise at implementation of computer drivers, online algorithms, control procedures. Basic ...
Added: October 13, 2016
, , , , in : Dynamics of Information Systems: Algorithmic Approaches. Vol. 51.: NY : Springer, 2013. P. 67-98.
Despite all the advantages brought by service-oriented architecture (SOA), experts argue that SOA introduces more complexity into information systems rather than resolving it. The problem of service integration challenges modern companies taking the risk of implementing SOA. One of important aspects of this problem relates to dynamic service composition, which has to take into account ...
Added: December 12, 2013