Naslov
Dense Time Multiset Rewriting Model in the Verification of Time-Sensitive Distributed Systems

Autori
Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn

Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, sažetak, znanstveni

Izvornik
Book of Abstracts / - , 2017, 25-26

Skup
Logic and Applications 2017

Mjesto i datum
Dubrovnik, Hrvatska, 18.09.2017. - 22.09.2017

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Multiset Rewriting, Distributed Systems, Computational Complexity, Maude, Real Time

Sažetak
We propose a Multiset Rewriting language with explicit dense (real) time for specifying and analysing Time-Sensitive Distributed Systems (TSDS). Discrete time models for the verification of TSDSes were introduced in [2]. Due to the foundational differences between models with discrete and models with real time [1], in the formal analysis of properties, such as security properties of Cyber- Physical Systems, some phenomena can only be captured by real time models. In order to specify dense time, we follow [1] in formalizing dense time in the multiset rewriting framework. We investigate real time TSDSes and their relevant properties and introduce adequate notions of time sampling and compliant traces. Properties of TSDSes are often specified using explicit time constraints which must be satisfied by the system perpetually. For example, drones carrying out the surveillance of some area must always have recent pictures of some points of interest. Possible environment interference (e.g., winds) are taken into account, e.g., autonomous drones achieve goals under possible interference of winds. Hence, we consider infinite traces over dense time domains in which goals are perpetually satisfied and which have some good properties with relation to time. Namely, we are interested in infinite traces which represent infinite periods of time where only a finite number of actions can be applied in any bounded time interval. One of the main challenges in the transition from discrete to dense time models of TSDSes is the additional non-determinism in the dense time model provided by the choice of a positive real value $\varepsilon$ in time advancement rule, $ Time@T \to Time@(T + \varepsilon)$, which may lead to Zeno type phenomena. We investigate properties of realizability (some trace is good) and survivability (where, in addition, all admissible traces are good) in models with dense time. We prove that for the class of progressive timed systems (PTS) both the realizability and the survivability problems have the same complexity as in the discrete time model case, both for infinite time versions as well as for the bounded time versions of the problems.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA