References of "Krstic, Srdan"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailA Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang et al

in Formal Methods in System Design (2019), 54(3), 279-335

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts ... [more ▼]

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification. [less ▲]

Detailed reference viewed: 136 (18 UL)
Full Text
Peer Reviewed
See detailOn the Risk of Tool Over-tuning in Runtime Verification Competitions
Bianculli, Domenico UL; Krstic, Srdan

in Proceedings of RV-CUBES 2017: an International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (2017, December 14)

Detailed reference viewed: 85 (13 UL)
Full Text
Peer Reviewed
See detailEfficient Large-scale Trace Checking Using MapReduce
Bersani, Marcello Maria; Bianculli, Domenico UL; Ghezzi, Carlo et al

in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016) (2016, May)

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic ... [more ▼]

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs. [less ▲]

Detailed reference viewed: 341 (24 UL)