crta
Hrvatska znanstvena Sekcija img
bibliografija
3 gif
 Naslovna
 O projektu
 FAQ
 Kontakt
4 gif
Pregledavanje radova
Jednostavno pretraživanje
Napredno pretraživanje
Skupni podaci
Upis novih radova
Upute
Ispravci prijavljenih radova
Ostale bibliografije
Slični projekti
 Bibliografske baze podataka

Pregled bibliografske jedinice broj: 894911

Zbornik radova

Autori: Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn
Naslov: Dense Time Multiset Rewriting Model in the Verification of Time-Sensitive Distributed Systems
Izvornik: Book of Abstracts
Skup: Logic and Applications 2017
Mjesto i datum: Dubrovnik, Hrvatska, 18-22.9.2017.
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.
Vrsta sudjelovanja: Predavanje
Vrsta prezentacije u zborniku: Sažetak
Vrsta recenzije: Međunarodna recenzija
Izvorni jezik: ENG
Kategorija: Znanstveni
Znanstvena područja:
Matematika,Računarstvo
Upisao u CROSBI: Tajana Ban Kirigin (bank@math.uniri.hr), 28. Ruj. 2017. u 22:03 sati



Verzija za printanje   za tiskati


upomoc
foot_4