arXiv subjects

Alberto Lluch Lafuente

Publications and source records attributed to Alberto Lluch Lafuente.

At least 19 recordsLinked to original sources

arXiv2026

Scaling Observation-aware Planning in Uncertain Domains

Deciding which sensing capabilities to deploy on an agent in uncertain domains is a fundamental engineering challenge, in which one balances task achievability against the high costs of hardware and processing. This problem has previously been formalized as the Optimal Observability Problem (OOP), based on the well-known Partially Observable Markov Decision Process (POMDP) model for decision-making. This work studies (sub-)symbolic techniques to scale solving of decidable fragments of the OOP, namely the Sensor Selection Problem (SSP) and the Positional Observability Problem (POP). Besides improving the original approach based on parameter synthesis, we develop a new solving method that identifies sensible observation functions via decomposition of POMDPs, improving performance by 3 and 5 orders of magnitude for instance size and runtime, respectively.

cs.AI↗

arXiv2024

Attack Tree Generation via Process Mining

Attack Trees are a graphical model of security used to study threat scenarios. While visually appealing and supported by solid theories and effective tools, one of their main drawbacks remains the amount of effort required by security experts to design them from scratch. This work aims to remedy this by providing a method for the automatic generation of Attack Trees from attack logs. The main original feature of our approach w.r.t existing ones is the use of Process Mining algorithms to synthesize Attack Trees, which allow users to customize the way a set of logs are summarized as an Attack Tree, for example by discarding statistically irrelevant events. Our approach is supported by a prototype that, apart from the derivation and translation of the model, provides the user with an Attack Tree in the RisQFLan format, a tool used for quantitative risk modeling and analysis with Attack Trees. We illustrate our approach with the case study of attacks on a communication protocol, produced by a state-of-the-art protocol analyzer.

cs.CR↗

arXiv2024

What should be observed for optimal reward in POMDPs?

Partially observable Markov Decision Processes (POMDPs) are a standard model for agents making decisions in uncertain environments. Most work on POMDPs focuses on synthesizing strategies based on the available capabilities. However, system designers can often control an agent's observation capabilities, e.g. by placing or selecting sensors. This raises the question of how one should select an agent's sensors cost-effectively such that it achieves the desired goals. In this paper, we study the novel optimal observability problem OOP: Given a POMDP M, how should one change M's observation capabilities within a fixed budget such that its (minimal) expected reward remains below a given threshold? We show that the problem is undecidable in general and decidable when considering positional strategies only. We present two algorithms for a decidable fragment of the OOP: one based on optimal strategies of M's underlying Markov decision process and one based on parameter synthesis with SMT. We report promising results for variants of typical examples from the POMDP literature.

cs.AI↗

arXiv2024

Assessing the Understandability and Acceptance of Attack-Defense Trees for Modelling Security Requirements

Context and Motivation Attack-Defense Trees (ADTs) are a graphical notation used to model and assess security requirements. ADTs are widely popular, as they can facilitate communication between different stakeholders involved in system security evaluation, and they are formal enough to be verified, e.g., with model checkers. Question/Problem While the quality of this notation has been primarily assessed quantitatively, its understandability has never been evaluated despite being mentioned as a key factor for its success. Principal idea/Results In this paper, we conduct an experiment with 25 human subjects to assess the understandability and user acceptance of the ADT notation. The study focuses on performance-based variables and perception-based variables, with the aim of evaluating the relationship between these measures and how they might impact the practical use of the notation. The results confirm a good level of understandability of ADTs. Participants consider them useful, and they show intention to use them. Contribution This is the first study empirically supporting the understandability of ADTs, thereby contributing to the theory of security requirements engineering.

cs.SE↗

arXiv2024

White-box validation of quantitative product lines by statistical model checking and process mining

We propose a novel methodology for validating software product line (PL) models by integrating Statistical Model Checking (SMC) with Process Mining (PM). Our approach focuses on the feature-oriented language QFLan in the PL engineering domain, allowing modeling of PLs with rich cross-tree and quantitative constraints, as well as aspects of dynamic PLs like staged configurations. This richness leads to models with infinite state-space, requiring simulation-based analysis techniques like SMC. For instance, we illustrate with a running example involving infinite state space. SMC involves generating samples of system dynamics to estimate properties such as event probabilities or expected values. On the other hand, PM uses data-driven techniques on execution logs to identify and reason about the underlying execution process. In this paper, we propose, for the first time, applying PM techniques to SMC simulations' byproducts to enhance the utility of SMC analyses. Typically, when SMC results are unexpected, modelers must determine whether they stem from actual system characteristics or model bugs in a black-box manner. We improve on this by using PM to provide a white-box perspective on the observed system dynamics. Samples from SMC are fed into PM tools, producing a compact graphical representation of observed dynamics. The mined PM model is then transformed into a QFLan model, accessible to PL engineers. Using two well-known PL models, we demonstrate the effectiveness and scalability of our methodology in pinpointing issues and suggesting fixes. Additionally, we show its generality by applying it to the security domain.

cs.SE↗

arXiv2023

Trust Management for Internet of Things: A Systematic Literature Review

Internet of Things (IoT) is a network of devices that communicate with each other through the internet and provides intelligence to industry and people. These devices are running in potentially hostile environments, so the need for security is critical. Trust Management aims to ensure the reliability of the network by assigning a trust value in every node indicating its trust level. This paper presents an exhaustive survey of the current Trust Management techniques for IoT, a classification based on the methods used in every work and a discussion of the open challenges and future research directions.

cs.NI↗

arXiv2023

A Survey of Automatic Generation of Attack Trees and Attack Graphs

Graphical security models constitute a well-known, user-friendly way to represent the security of a system. These kinds of models are used by security experts to identify vulnerabilities and assess the security of a system. The manual construction of these models can be tedious, especially for large enterprises. Consequently, the research community is trying to address this issue by proposing methods for the automatic generation of such models. In this work, we present a survey illustrating the current status of the automatic generation of two kinds of graphical security models -Attack Trees and Attack Graphs. The goal of this survey is to present the current methodologies used in the field, compare them and present the challenges and future directions for the research community.

cs.CR↗

arXiv2023

Minimization of Dynamical Systems over Monoids

Quantitative notions of bisimulation are well-known tools for the minimization of dynamical models such as Markov chains and ordinary differential equations (ODEs). In \emph{forward bisimulations}, each state in the quotient model represents an equivalence class and the dynamical evolution gives the overall sum of its members in the original model. Here we introduce generalized forward bisimulation (GFB) for dynamical systems over commutative monoids and develop a partition refinement algorithm to compute the coarsest one. When the monoid is $(\mathbb{R}, +)$, we recover probabilistic bisimulation for Markov chains and more recent forward bisimulations for nonlinear ODEs. Using $(\mathbb{R}, \cdot)$ we get nonlinear reductions for discrete-time dynamical systems and ODEs where each variable in the quotient model represents the product of original variables in the equivalence class. When the domain is a finite set such as the Booleans $\mathbb{B}$, we can apply GFB to Boolean networks (BN), a widely used dynamical model in computational biology. Using a prototype implementation of our minimization algorithm for GFB, we find disjunction- and conjunction-preserving reductions on 60 BN from two well-known repositories, and demonstrate the obtained analysis speed-ups. We also provide the biological interpretation of the reduction obtained for two selected BN, and we show how GFB enables the analysis of a large one that could not be analyzed otherwise. Using a randomized version of our algorithm we find product-preserving (therefore non-linear) reductions on 21 dynamical weighted networks from the literature that could not be handled by the exact algorithm.

cs.LO↗

arXiv2022

Formal Analysis of Lending Pools in Decentralized Finance

Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi applications is essential to assess their safety. We have developed a tool for the formal analysis of one of the most widespread DeFi applications: Lending Pools (LP). This was achieved by leveraging an existing formal model for LPs, the Maude verification environment and the MultiVeStA statistical analyser. The tool supports several analyses including reachability analysis, LTL model checking and statistical model checking. In this paper we show how the tool can be used to analyse several parameters of LPs that are fundamental to assess and predict their behaviour. In particular, we use statistical analysis to search for threshold and reward parameters that minimize the risk of unrecoverable loans.

cs.SE↗

arXiv2021

Reducing Boolean Networks with Backward Boolean Equivalence

Boolean Networks (BNs) are established models to qualitatively describe biological systems. The analysis of BNs might be infeasible for medium to large BNs due to the state-space explosion problem. We propose a novel reduction technique called \emph{Backward Boolean Equivalence} (BBE), which preserves some properties of interest of BNs. In particular, reduced BNs provide a compact representation by grouping variables that, if initialized equally, are always updated equally. The resulting reduced state space is a subset of the original one, restricted to identical initialization of grouped variables. The corresponding trajectories of the original BN can be exactly restored. We show the effectiveness of BBE by performing a large-scale validation on the whole GINsim BN repository. In selected cases, we show how our method enables analyses that would be otherwise intractable. Our method complements, and can be combined with, other reduction methods found in the literature.

cs.CE↗

arXiv2021

Quantitative Security Risk Modeling and Analysis with RisQFLan

Domain-specific quantitative modeling and analysis approaches are fundamental in scenarios in which qualitative approaches are inappropriate or unfeasible. In this paper, we present a tool-supported approach to quantitative graph-based security risk modeling and analysis based on attack-defense trees. Our approach is based on QFLan, a successful domain-specific approach to support quantitative modeling and analysis of highly configurable systems, whose domain-specific components have been decoupled to facilitate the instantiation of the QFLan approach in the domain of graph-based security risk modeling and analysis. Our approach incorporates distinctive features from three popular kinds of attack trees, namely enhanced attack trees, capabilities-based attack trees and attack countermeasure trees, into the domain-specific modeling language. The result is a new framework, called RisQFLan, to support quantitative security risk modeling and analysis based on attack-defense diagrams. By offering either exact or statistical verification of probabilistic attack scenarios, RisQFLan constitutes a significant novel contribution to the existing toolsets in that domain. We validate our approach by highlighting the additional features offered by RisQFLan in three illustrative case studies from seminal approaches to graph-based security risk modeling analysis based on attack trees.

cs.CR↗

arXiv2018

A framework for quantitative modeling and analysis of highly (re)configurable systems

This paper presents our approach to the quantitative modeling and analysis of highly (re)configurable systems, such as software product lines. Different combinations of the optional features of such a system give rise to combinatorially many individual system variants. We use a formal modeling language that allows us to model systems with probabilistic behavior, possibly subject to quantitative feature constraints, and able to dynamically install, remove or replace features. More precisely, our models are defined in the probabilistic feature-oriented language QFLAN, a rich domain specific language (DSL) for systems with variability defined in terms of features. QFLAN specifications are automatically encoded in terms of a process algebra whose operational behavior interacts with a store of constraints, and hence allows to separate system configuration from system behavior. The resulting probabilistic configurations and behavior converge seamlessly in a semantics based on discrete-time Markov chains, thus enabling quantitative analysis. Our analysis is based on statistical model checking techniques, which allow us to scale to larger models with respect to precise probabilistic analysis techniques. The analyses we can conduct range from the likelihood of specific behavior to the expected average cost, in terms of feature attributes, of specific system variants. Our approach is supported by a novel Eclipse-based tool which includes state-of-the-art DSL utilities for QFLAN based on the Xtext framework as well as analysis plug-ins to seamlessly run statistical model checking analyses. We provide a number of case studies that have driven and validated the development of our framework.

cs.SE↗

arXiv2017

Microservices: yesterday, today, and tomorrow

Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Before presenting the current state-of-the-art in the field, this chapter reviews the history of software architecture, the reasons that led to the diffusion of objects and services first, and microservices later. Finally, open problems and future challenges are introduced. This survey primarily addresses newcomers to the discipline, while offering an academic viewpoint on the topic. In addition, we investigate some practical issues and point out some potential solutions.

cs.SE↗

arXiv2017

Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields

Coordination is essential for dynamic distributed systems whose components exhibit interactive and autonomous behaviors. Spatially distributed, locally interacting, propagating computational fields are particularly appealing for allowing components to join and leave with little or no overhead. Computational fields are a key ingredient of aggregate programming, a promising software engineering methodology particularly relevant for the Internet of Things. In our approach, space topology is represented by a fixed graph-shaped field, namely a network with attributes on both nodes and arcs, where arcs represent interaction capabilities between nodes. We propose a SMuC calculus where mu-calculus- like modal formulas represent how the values stored in neighbor nodes should be combined to update the present node. Fixpoint operations can be understood globally as recursive definitions, or locally as asynchronous converging propagation processes. We present a distributed implementation of our calculus. The translation is first done mapping SMuC programs into normal form, purely iterative programs and then into distributed programs. Some key results are presented that show convergence of fixpoint computations under fair asynchrony and under reinitialization of nodes. The first result allows nodes to proceed at different speeds, while the second one provides robustness against certain kinds of failure. We illustrate our approach with a case study based on a disaster recovery scenario, implemented in a prototype simulator that we use to evaluate the performance of a recovery strategy.

cs.LO↗

arXiv2017

A Coordination Language for Databases

We present a coordination language for the modeling of distributed database applications. The language, baptized Klaim-DB, borrows the concepts of localities and nets of the coordination language Klaim but re-incarnates the tuple spaces of Klaim as databases. It provides high-level abstractions and primitives for the access and manipulation of structured data, with integrity and atomicity considerations. We present the formal semantics of Klaim-DB and develop a type system that avoids potential runtime errors such as certain evaluation errors and mismatches of data format in tables, which are monitored in the semantics. The use of the language is illustrated in a scenario where the sales from different branches of a chain of department stores are aggregated from their local databases. Raising the abstraction level and encapsulating integrity checks in the language primitives have benefited the modeling task considerably.

cs.LO↗

arXiv2015

Proceedings 8th Interaction and Concurrency Experience

This volume contains the proceedings of ICE 2015, the 8th Interaction and Concurrency Experience, which was held in Grenoble, France on the 4th and 5th of June 2015 as a satellite event of DisCoTec 2015. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum with access restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions to which the authors reply. Each paper was reviewed by three PC members, and altogether 9 papers, including 1 short paper, were accepted for publication (the workshop also featured 4 brief announcements which are not part of this volume). We were proud to host three invited talks, by Leslie Lamport (shared with the FRIDA workshop), Joseph Sifakis and Steve Ross-Talbot. The abstracts of the last two talks are included in this volume together with the regular papers.

cs.PL↗

arXiv2015

Proceedings 11th International Workshop on Automated Specification and Verification of Web Systems

These proceedings contain the papers presented at the 11th International Workshop on Automated Specification and Verification of Web Systems (WWV 2015), which was held on 23 June 2015 in Oslo, Norway, as a satellite workshop of the 20th International Symposium on Formal Methods (FM 2015). WWV is a yearly interdisciplinary forum for researchers originating from the following areas: declarative, rule-based programming, formal methods, software engineering and web-based systems. The workshop fosters the cross-fertilisation and advancement of hybrid methods from such areas.

cs.LO↗

arXiv2015

Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking

We investigate the suitability of statistical model checking techniques for analysing quantitative properties of software product line models with probabilistic aspects. For this purpose, we enrich the feature-oriented language FLan with action rates, which specify the likelihood of exhibiting particular behaviour or of installing features at a specific moment or in a specific order. The enriched language (called PFLan) allows us to specify models of software product lines with probabilistic configurations and behaviour, e.g. by considering a PFLan semantics based on discrete-time Markov chains. The Maude implementation of PFLan is combined with the distributed statistical model checker MultiVeStA to perform quantitative analyses of a simple product line case study. The presented analyses include the likelihood of certain behaviour of interest (e.g. product malfunctioning) and the expected average cost of products.

cs.SE↗