Jaime Arias

Jaime Arias, Kyungmin Bae, Carlos Olarte et al.

This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases.

Jaime Arias, Carlos E. Budde, Wojciech Penczek et al.

Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-Agents Systems--EAMAS. The ADT-EAMAS transformation is performed in a systematic manner that ensures correctness. The transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools.