Zobrazeno 1 - 10
of 43
pro vyhledávání: '"Felix Klaedtke"'
Autor:
Ghada Arfaoui, Pascal Bisson, Rolf Blom, Ravishankar Borgaonkar, Hakan Englund, Edith Felix, Felix Klaedtke, Prajwol Kumar Nakarmi, Mats Naslund, Piers O'Hanlon, Juri Papay, Jani Suomalainen, Mike Surridge, Jean-Philippe Wary, Alexander Zahariev
Publikováno v:
IEEE Access, Vol 6, Pp 22466-22479 (2018)
5G networks will provide opportunities for the creation of new services, for new business models, and for new players to enter the mobile market. The networks will support efficient and cost-effective launch of a multitude of services, tailored for d
Externí odkaz:
https://doaj.org/article/876591b1b0cf4068a488a7b55ff287b2
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 96, Iss Proc. GandALF 2012, Pp 113-126 (2012)
It is known that the alternation hierarchy of least and greatest fixpoint operators in the mu-calculus is strict. However, the strictness of the alternation hierarchy does not necessarily carry over when considering restricted classes of structures.
Externí odkaz:
https://doaj.org/article/5c61111f76b0452ca050329156af9a58
Publikováno v:
Formal Methods in System Design, 46 (3)
In system monitoring, one is often interested in checking properties of aggregated data. Current policy monitoring approaches are limited in the kinds of aggregations they handle. To rectify this, we extend an expressive language, metric first-order
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::873e40f2bb6e29a70f08ac180dd260f2
http://doc.rero.ch/record/331126/files/10703_2015_Article_222.pdf
http://doc.rero.ch/record/331126/files/10703_2015_Article_222.pdf
Publikováno v:
Acta Informatica. 55:309-338
Real-time logics are popular specification languages for reasoning about systems intended to meet timing constraints. Numerous formalisms have been proposed with different underlying time models that can be characterized along two dimensions: dense v
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c970c3854ca056e369ef93c1abb7cde6
https://doi.org/10.1007/s00236-017-0295-4
https://doi.org/10.1007/s00236-017-0295-4
We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where messages can be delayed, reordered, or even lost. Furthermore, our approach h
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c46e685ddb7ac99b80f171b52aa288fa
Publikováno v:
Formal Methods in System Design. 49:75-108
We propose an approach to monitoring IT systems offline where system actions are logged in a distributed file system and subsequently checked for compliance against policies formulated in an expressive temporal logic. The novelty of our approach is t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1f58d0878bb315960d4a2dc9d53f94a5
https://doi.org/10.1007/s10703-016-0242-y
https://doi.org/10.1007/s10703-016-0242-y
Publikováno v:
RV-CuBES
MonPoly is a monitoring tool for checking logs against formulas of metric first-order temporal logic. We provide here an overview of the tool, including its usage and history.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e04ae67be823c384fca80a060a42c7d6
https://doi.org/10.29007/89hs
https://doi.org/10.29007/89hs
Publikováno v:
ACM Transactions on Computational Logic. 16:1-24
Checking whether one formal language is included in another is important in many verification tasks. In this article, we provide solutions for checking the inclusion of languages given by visibly pushdown automata over both finite and infinite words.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::17cf818f0b274c8f21badea52785ec9f
https://doi.org/10.1145/2774221
https://doi.org/10.1145/2774221
Publikováno v:
Journal of the ACM. 62:1-45
Runtime monitoring is a general approach to verifying system properties at runtime by comparing system events against a specification formalizing which event sequences are allowed. We present a runtime monitoring algorithm for a safety fragment of me
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8bbed57f92271096b3e5e0b6f72c591a
https://doi.org/10.1145/2699444
https://doi.org/10.1145/2699444
Publikováno v:
Information Processing Letters. 114:680-688
We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::13098c71f941e1c5de44d931e2e4e677
https://doi.org/10.1016/j.ipl.2014.06.005
https://doi.org/10.1016/j.ipl.2014.06.005