-
On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
Authors:
Mikael Bisgaard Dahlsen-Jensen,
Baptiste Fievet,
Laure Petrucci,
Jaco van de Pol
Abstract:
Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for…
▽ More
Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations ``in the limit''.
△ Less
Submitted 20 January, 2024;
originally announced January 2024.
-
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
Authors:
Jaime Arias,
Kyungmin Bae,
Carlos Olarte,
Peter Csaba Ölveczky,
Laure Petrucci
Abstract:
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 comp…
▽ More
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.
△ Less
Submitted 5 April, 2024; v1 submitted 3 January, 2024;
originally announced January 2024.
-
Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models
Authors:
Jaime Arias,
Carlos Olarte,
Laure Petrucci,
Łukasz Maśko,
Wojciech Penczek,
Teofil Sidoruk
Abstract:
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn…
▽ More
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using Rewriting Logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialised algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks.
△ Less
Submitted 19 October, 2023; v1 submitted 8 May, 2023;
originally announced May 2023.
-
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
Authors:
Jaime Arias,
Kyungmin Bae,
Carlos Olarte,
Peter Csaba Ölveczky,
Laure Petrucci,
Fredrik Rømming
Abstract:
Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding a…
▽ More
Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Roméo can be done in 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 on three benchmarks show that our methods outperform Roméo in many cases.
△ Less
Submitted 15 March, 2023;
originally announced March 2023.
-
Strategic (Timed) Computation Tree Logic
Authors:
Jaime Arias,
Wojciech Jamroga,
Wojciech Penczek,
Laure Petrucci,
Teofil Sidoruk
Abstract:
We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding inform…
▽ More
We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTL[ir] is of the same complexity as for ATL[ir], the model checking problem for STCTL[ir] is of the same complexity as for TCTL, while for STCTL[iR] it is undecidable as for ATL[iR]. The above results suggest to use SCTL[ir] and STCTL[ir] in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTL[ir].
△ Less
Submitted 19 October, 2023; v1 submitted 26 February, 2023;
originally announced February 2023.
-
Efficient Convex Zone Merging in Parametric Timed Automata
Authors:
Étienne André,
Dylan Marinho,
Laure Petrucci,
Jaco van de Pol
Abstract:
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while pres…
▽ More
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.
△ Less
Submitted 9 December, 2022;
originally announced December 2022.
-
Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees
Authors:
Jaime Arias,
Łukasz Maśko,
Wojciech Penczek,
Laure Petrucci,
Teofil Sidoruk
Abstract:
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn…
▽ More
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using minimal number of agents for a given attack-defence tree.
△ Less
Submitted 29 April, 2022; v1 submitted 17 January, 2021;
originally announced January 2021.
-
Modular Analysis of Tree-Topology Models
Authors:
Laure Petrucci,
Michał Knapik
Abstract:
We investigate networks of automata that synchronise over common action labels. A graph synchronisation topology between the automata is defined in such a way that two automata are connected iff they can synchronise over an action. We show a very effective reduction of networks of automata with tree-like synchronisation topologies. The reduction preserves a certain form of reachability, but not sa…
▽ More
We investigate networks of automata that synchronise over common action labels. A graph synchronisation topology between the automata is defined in such a way that two automata are connected iff they can synchronise over an action. We show a very effective reduction of networks of automata with tree-like synchronisation topologies. The reduction preserves a certain form of reachability, but not safety. The procedure is implemented in an open-source tool.
△ Less
Submitted 8 December, 2020;
originally announced December 2020.
-
hXDP: Efficient Software Packet Processing on FPGA NICs
Authors:
Marco Spaziani Brunella,
Giacomo Belocchi,
Marco Bonola,
Salvatore Pontarelli,
Giuseppe Siracusano,
Giuseppe Bianchi,
Aniello Cammarano,
Alessandro Palumbo,
Luca Petrucci,
Roberto Bifulco
Abstract:
FPGA accelerators on the NIC enable the offloading of expensive packet processing tasks from the CPU. However, FPGAs have limited resources that may need to be shared among diverse applications, and programming them is difficult.
We present a solution to run Linux's eXpress Data Path programs written in eBPF on FPGAs, using only a fraction of the available hardware resources while matching the p…
▽ More
FPGA accelerators on the NIC enable the offloading of expensive packet processing tasks from the CPU. However, FPGAs have limited resources that may need to be shared among diverse applications, and programming them is difficult.
We present a solution to run Linux's eXpress Data Path programs written in eBPF on FPGAs, using only a fraction of the available hardware resources while matching the performance of high-end CPUs. The iterative execution model of eBPF is not a good fit for FPGA accelerators. Nonetheless, we show that many of the instructions of an eBPF program can be compressed, parallelized or completely removed, when targeting a purpose-built FPGA executor, thereby significantly improving performance. We leverage that to design hXDP, which includes (i) an optimizing-compiler that parallelizes and translates eBPF bytecode to an extended eBPF Instruction-set Architecture defined by us; a (ii) soft-CPU to execute such instructions on FPGA; and (iii) an FPGA-based infrastructure to provide XDP's maps and helper functions as defined within the Linux kernel.
We implement hXDP on an FPGA NIC and evaluate it running real-world unmodified eBPF programs. Our implementation is clocked at 156.25MHz, uses about 15% of the FPGA resources, and can run dynamically loaded programs. Despite these modest requirements, it achieves the packet processing throughput of a high-end CPU core and provides a 10x lower packet forwarding latency.
△ Less
Submitted 27 October, 2020;
originally announced October 2020.
-
Parametric Verification: An Introduction
Authors:
Étienne André,
Michał Knapik,
Didier Lime,
Wojciech Penczek,
Laure Petrucci
Abstract:
This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toruń (2016) and Zaragoza (2017). The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area.
We…
▽ More
This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toruń (2016) and Zaragoza (2017). The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area.
We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.
△ Less
Submitted 1 July, 2019;
originally announced July 2019.
-
Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems
Authors:
Jaime Arias,
Carlos E. Budde,
Wojciech Penczek,
Laure Petrucci,
Mariëlle Stoelinga
Abstract:
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-A…
▽ More
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.
△ Less
Submitted 12 June, 2019;
originally announced June 2019.
-
Minimal-Time Synthesis for Parametric Timed Automata
Authors:
Étienne André,
Vincent Bloemen,
Laure Petrucci,
Jaco van de Pol
Abstract:
Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks.
We focu…
▽ More
Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks.
We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter values can we achieve this? We analyse the problem and present an algorithm that solves it. We also discuss and provide solutions for minimizing a specific parameter value to still reach the goal.
We empirically study the performance of these algorithms on a benchmark set for PTAs and show that minimal-time reachability synthesis is more efficient to compute than the standard synthesis algorithm for reachability.
△ Less
Submitted 8 February, 2019;
originally announced February 2019.
-
Quasi-Optimal Partial Order Reduction
Authors:
Huyen T. T Nguyen,
César Rodríguez,
Marcelo Sousa,
Camille Coti,
Laure Petrucci
Abstract:
A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with $\mathop{\mathcal{O}}(n)$ Mazurkiewicz traces where SDPOR explores…
▽ More
A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with $\mathop{\mathcal{O}}(n)$ Mazurkiewicz traces where SDPOR explores $\mathop{\mathcal{O}}(2^n)$ redundant schedules and identify the cause of the blow-up as an NP-hard problem. Our main contribution is a new approach, called Quasi-Optimal POR, that can arbitrarily approximate an optimal exploration using a provided constant k. We present an implementation of our method in a new tool called Dpu using specialised data structures. Experiments with Dpu, including Debian packages, show that optimality is achieved with low values of k, outperforming state-of-the-art tools.
△ Less
Submitted 20 April, 2018; v1 submitted 12 February, 2018;
originally announced February 2018.
-
Towards a Stateful Forwarding Abstraction to Implement Scalable Network Functions in Software and Hardware
Authors:
Luca Petrucci,
Nicola Bonelli,
Marco Bonola,
Gregorio Procissi,
Carmelo Cascone,
Davide Sanvito,
Salvatore Pontarelli,
Giuseppe Bianchi,
Roberto Bifulco
Abstract:
An effective packet processing abstraction that leverages software or hardware acceleration techniques can simplify the implementation of high-performance virtual network functions. In this paper, we explore the suitability of SDN switches' stateful forwarding abstractions to model accelerated functions in both software and hardware accelerators, such as optimized software switches and FPGA-based…
▽ More
An effective packet processing abstraction that leverages software or hardware acceleration techniques can simplify the implementation of high-performance virtual network functions. In this paper, we explore the suitability of SDN switches' stateful forwarding abstractions to model accelerated functions in both software and hardware accelerators, such as optimized software switches and FPGA-based NICs. In particular, we select an Extended Finite State Machine abstraction and demonstrate its suitability by implementing the Linux's iptables interface. By doing so, we provide the acceleration of functions such as stateful firewalls, load balancers and dynamic NATs. We find that supporting a flow-level programming consistency model is an important feature of a programming abstraction in this context. Furthermore, we demonstrate that such a model simplifies the scaling of the system when implemented in software, enabling efficient multi-core processing without harming state consistency.
△ Less
Submitted 9 November, 2016;
originally announced November 2016.
-
Formally Proving and Enhancing a Self-Stabilising Distributed Algorithm
Authors:
Camille Coti,
Charles Lakos,
Laure Petrucci
Abstract:
This paper presents the benefits of formal modelling and verification techniques for self-stabilising distributed algorithms. An algorithm is studied, that takes a set of processes connected by a tree topology and converts it to a ring configuration. The Coloured Petri net model not only facilitates the proof that the algorithm is correct and self-stabilising but also easily shows that it enjoys n…
▽ More
This paper presents the benefits of formal modelling and verification techniques for self-stabilising distributed algorithms. An algorithm is studied, that takes a set of processes connected by a tree topology and converts it to a ring configuration. The Coloured Petri net model not only facilitates the proof that the algorithm is correct and self-stabilising but also easily shows that it enjoys new properties of termination and silentness. Further, the formal results show how the algorithm can be simplified without loss of generality.
△ Less
Submitted 14 January, 2016;
originally announced January 2016.
-
Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications
Authors:
Shang-Wei Lin,
Laure Petrucci
Abstract:
This volume contains the proceedings of the 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA'14). The workshop was held in Singapore on May 13th, 2014, as a satellite event of the 19th International Symposium on Formal Methods (FM'14).
FSFMA aims at sharing research interests and launching collaborations in the area of formal methods and their applications. The scientifi…
▽ More
This volume contains the proceedings of the 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA'14). The workshop was held in Singapore on May 13th, 2014, as a satellite event of the 19th International Symposium on Formal Methods (FM'14).
FSFMA aims at sharing research interests and launching collaborations in the area of formal methods and their applications. The scientific subject of the workshop covers (but is not limited to) areas such as formal specification, model checking, verification, program analysis/transformation, software engineering, and applications in major areas of computer science, including aeronautics and aerospace. The workshop brings together researchers and industry R&D experts from France, Singapore and other countries together to exchange their knowledge, discuss their research findings, and explore potential collaborations.
This volume contains eight contributions: four invited talks and four regular papers.
△ Less
Submitted 8 July, 2014;
originally announced July 2014.