-
Assessing the Understandability and Acceptance of Attack-Defense Trees for Modelling Security Requirements
Authors:
Giovanna Broccia,
Maurice H. ter Beek,
Alberto Lluch Lafuente,
Paola Spoletini,
Alessio Ferrari
Abstract:
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 as…
▽ More
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.
△ Less
Submitted 9 April, 2024;
originally announced April 2024.
-
Strategies, Benefits and Challenges of App Store-inspired Requirements Elicitation
Authors:
Alessio Ferrari,
Paola Spoletini
Abstract:
App store-inspired elicitation is the practice of exploring competitors' apps, to get inspiration for requirements. This activity is common among developers, but little insight is available on its practical use, advantages, and possible issues. This paper aims to study strategies, benefits, and challenges of app store-inspired elicitation, and to compare this technique with the more traditional re…
▽ More
App store-inspired elicitation is the practice of exploring competitors' apps, to get inspiration for requirements. This activity is common among developers, but little insight is available on its practical use, advantages, and possible issues. This paper aims to study strategies, benefits, and challenges of app store-inspired elicitation, and to compare this technique with the more traditional requirements elicitation interviews. We conduct an experimental simulation with 58 analysts and collect qualitative data. Our results show that: (1) specific guidelines and procedures are required to better conduct app store-inspired elicitation; (2) current search features made available by app stores are not suitable for this practice, and more tool support is required to help analysts in the retrieval and evaluation of competing products; (3) while interviews focus on the why dimension of requirements engineering (i.e., goals), app store-inspired elicitation focuses on how (i.e., solutions), offering indications for implementation and improved usability. Our study provides a framework for researchers to address existing challenges and suggests possible benefits to foster app store-inspired elicitation among practitioners.
△ Less
Submitted 28 January, 2023;
originally announced January 2023.
-
How Do Requirements Evolve During Elicitation? An Empirical Study Combining Interviews and App Store Analysis
Authors:
Alessio Ferrari,
Paola Spoletini,
Sourav Debnath
Abstract:
Requirements are elicited from the customer and other stakeholders through an iterative process of interviews, prototy**, and other interactive sessions. Then, requirements can be further extended, based on the analysis of the features of competing products available on the market. Understanding how this process takes place can help to identify the contribution of the different elicitation phase…
▽ More
Requirements are elicited from the customer and other stakeholders through an iterative process of interviews, prototy**, and other interactive sessions. Then, requirements can be further extended, based on the analysis of the features of competing products available on the market. Understanding how this process takes place can help to identify the contribution of the different elicitation phases, thereby allowing requirements analysts to better distribute their resources. In this work, we empirically study in which way requirements get transformed from initial ideas into documented needs, and then evolve based on the inspiration coming from similar products. To this end, we select 30 subjects that act as requirements analysts, and we perform interview-based elicitation sessions with a fictional customer. After the sessions, the analysts produce a first set of requirements for the system. Then, they are required to search similar products in the app stores, and extend the requirements, inspired by the identified apps. The requirements documented at each step are evaluated, to assess to which extent and in which way the initial idea evolved throughout the process. Our results show that only between 30\% and 38\% of the requirements produced after the interviews include content that can be fully traced to initial customer's ideas. Furthermore, up to 42\% of the requirements inspired by the app stores cover additional features compared to the ones identified after the interviews. The results empirically show that requirements are not elicited in strict sense, but actually co-created through interviews, with analysts playing a crucial role in the process. In addition, we show evidence that app store-inspired elicitation can be particularly beneficial to complete the requirements.
△ Less
Submitted 1 August, 2022;
originally announced August 2022.
-
Using Voice and Biofeedback to Predict User Engagement during Product Feedback Interviews
Authors:
Alessio Ferrari,
Thaide Huichapa,
Paola Spoletini,
Nicole Novielli,
Davide Fucci,
Daniela Girardi
Abstract:
Capturing users' engagement is crucial for gathering feedback about the features of a software product. In a market-driven context, current approaches to collect and analyze users' feedback are based on techniques leveraging information extracted from product reviews and social media. These approaches are hardly applicable in bespoke software development, or in contexts in which one needs to gathe…
▽ More
Capturing users' engagement is crucial for gathering feedback about the features of a software product. In a market-driven context, current approaches to collect and analyze users' feedback are based on techniques leveraging information extracted from product reviews and social media. These approaches are hardly applicable in bespoke software development, or in contexts in which one needs to gather information from specific users. In such cases, companies need to resort to face-to-face interviews to get feedback on their products. In this paper, we propose to utilize biometric data, in terms of physiological and voice features, to complement interviews with information about the engagement of the user on the discussed product-relevant topics. We evaluate our approach by interviewing users while gathering their physiological data (i.e., biofeedback) using an Empatica E4 wristband, and capturing their voice through the default audio-recorder of a common laptop. Our results show that we can predict users' engagement by training supervised machine learning algorithms on biometric data (F1=0.72), and that voice features alone are sufficiently effective (F1=0.71). Our work contributes with one the first studies in requirements engineering in which biometrics are used to identify emotions. This is also the first study in software engineering that considers voice analysis. The usage of voice features could be particularly helpful for emotion-aware requirements elicitation in remote communication, either performed by human analysts or voice-based chatbots, and can also be exploited to support the analysis of meetings in software engineering research.
△ Less
Submitted 1 July, 2024; v1 submitted 6 April, 2021;
originally announced April 2021.
-
Optimal by Design: Model-Driven Synthesis of Adaptation Strategies for Autonomous Systems
Authors:
Yehia Elrakaiby,
Paola Spoletini,
Bashar Nuseibeh
Abstract:
Many software systems have become too large and complex to be managed efficiently by human administrators, particularly when they operate in uncertain and dynamic environments and require frequent changes. Requirements-driven adaptation techniques have been proposed to endow systems with the necessary means to autonomously decide ways to satisfy their requirements. However, many current approaches…
▽ More
Many software systems have become too large and complex to be managed efficiently by human administrators, particularly when they operate in uncertain and dynamic environments and require frequent changes. Requirements-driven adaptation techniques have been proposed to endow systems with the necessary means to autonomously decide ways to satisfy their requirements. However, many current approaches rely on general-purpose languages, models and/or frameworks to design, develop and analyze autonomous systems. Unfortunately, these tools are not tailored towards the characteristics of adaptation problems in autonomous systems. In this paper, we present Optimal by Design (ObD ), a framework for model-based requirements-driven synthesis of optimal adaptation strategies for autonomous systems. ObD proposes a model (and a language) for the high-level description of the basic elements of self-adaptive systems, namely the system, capabilities, requirements and environment. Based on those elements, a Markov Decision Process (MDP) is constructed to compute the optimal strategy or the most rewarding system behaviour. Furthermore, this defines a reflex controller that can ensure timely responses to changes. One novel feature of the framework is that it benefits both from goal-oriented techniques, developed for requirement elicitation, refinement and analysis, and synthesis capabilities and extensive research around MDPs, their extensions and tools. Our preliminary evaluation results demonstrate the practicality and advantages of the framework.
△ Less
Submitted 16 January, 2020;
originally announced January 2020.
-
From model checking to a temporal proof for partial models: preliminary example
Authors:
A. Bernasconi,
C. Menghi,
P. Spoletini,
L. D. Zuck,
C. Ghezzi
Abstract:
This paper describes in detail the example introduced in the preliminary evaluation of THRIVE. Specifically, it evaluates THRIVE over an abstraction of the ground model proposed for a critical component belonging to a medical device used by optometrists and ophtalmologits to dected visual problems.
This paper describes in detail the example introduced in the preliminary evaluation of THRIVE. Specifically, it evaluates THRIVE over an abstraction of the ground model proposed for a critical component belonging to a medical device used by optometrists and ophtalmologits to dected visual problems.
△ Less
Submitted 8 June, 2017;
originally announced June 2017.
-
Modeling, refining and analyzing Incomplete Büchi Automata
Authors:
Claudio Menghi,
Paola Spoletini,
Carlo Ghezzi
Abstract:
Software development is an iterative process which includes a set of development steps that transform the initial high level specification of the system into its final, fully specified, implementation. This report discusses the theoretical foundations that allow Incomplete Büchi Automata (IBAs) to be used in the iterative development of a sequential system.
Software development is an iterative process which includes a set of development steps that transform the initial high level specification of the system into its final, fully specified, implementation. This report discusses the theoretical foundations that allow Incomplete Büchi Automata (IBAs) to be used in the iterative development of a sequential system.
△ Less
Submitted 2 September, 2016;
originally announced September 2016.
-
Bounded Variability of Metric Temporal Logic
Authors:
Carlo A. Furia,
Paola Spoletini
Abstract:
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability---where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the…
▽ More
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability---where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability?
In this paper, we study the problem with reference to Metric Temporal Logic (MTL). We prove that deciding bounded variability of MTL formulas is undecidable over dense-time models, but with a undecidability degree lower than generic dense-time MTL satisfiability. Over discrete-time models, instead, deciding MTL bounded variability has the same exponential-space complexity as satisfiability. To complement these negative results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability.
△ Less
Submitted 4 July, 2014; v1 submitted 10 June, 2013;
originally announced June 2013.
-
Fuzzy Time in LTL
Authors:
Achille Frigeri,
Liliana Pasquale,
Paola Spoletini
Abstract:
In the last years, the adoption of active systems has increased in many fields of computer science, such as databases, sensor networks, and software engineering. These systems are able to automatically react to events, by collecting information from outside and internally generating new events. However, the collection of data is often hampered by uncertainty and vagueness that can arise from the i…
▽ More
In the last years, the adoption of active systems has increased in many fields of computer science, such as databases, sensor networks, and software engineering. These systems are able to automatically react to events, by collecting information from outside and internally generating new events. However, the collection of data is often hampered by uncertainty and vagueness that can arise from the imprecision of the monitoring infrastructure, unreliable data sources, and networks. The decision making mechanism used to produce a reaction is also imprecise, and cannot be evaluated in a crisp way. It depends on the evaluation of vague temporal constraints, which are expressed on the collected data by humans. Despite fuzzy logic has been mainly conceived as a mathematical abstraction to express vagueness, no attempt has been made to fuzzify the temporal modalities. Existing fuzzy languages do not allow us to represent temporal properties, such as "almost always" and "soon". Indeed, the semantics of existing fuzzy temporal operators is based on the idea of replacing classical connectives or propositions with their fuzzy counterparts. To overcome these limitations, we propose a temporal framework, FTL (Fuzzy-time Temporal Logic), to express vagueness on time. This framework formally defines a set of fuzzy temporal modalities, which can be customized by choosing a specific semantics for the connectives. The semantics of the language is sound, and the introduced modalities respect a set of expected mutual relations. We also prove that under the assumption that all events are crisp, FTL reduces to LTL. Finally, for some of the possible fuzzy interpretations of the connectives, we identify adequate sets of temporal operators, from which it is possible to derive all the others.
△ Less
Submitted 28 March, 2012;
originally announced March 2012.
-
Proceedings 2nd Interaction and Concurrency Experience: Structured Interactions
Authors:
Filippo Bonchi,
Davide Grohmann,
Paola Spoletini,
Emilio Tuosto
Abstract:
This volume contains the proceedings of the 2nd Workshop on Interaction and Concurrency Experience (ICE'09). The workshop was held in Bologna, Italy on 31th of August 2009, as a satellite workshop of CONCUR'09. The previous edition of ICE has been organized in Reykjavik (2008).
The ICE workshop is intended as a series of international scientific meetings oriented to researchers in various fiel…
▽ More
This volume contains the proceedings of the 2nd Workshop on Interaction and Concurrency Experience (ICE'09). The workshop was held in Bologna, Italy on 31th of August 2009, as a satellite workshop of CONCUR'09. The previous edition of ICE has been organized in Reykjavik (2008).
The ICE workshop is intended as a series of international scientific meetings oriented to researchers in various fields of theoretical computer science and, each year, the workshop focuses on a specific topic: ICE 2009 focused on structured interactions meant as the class of synchronisations that go beyond the "simple" point-to-point synchronisations (e.g., multicast or broadcast synchronisations, even-notification based interactions, time dependent interactions, distributed transactions,...).
△ Less
Submitted 3 December, 2009;
originally announced December 2009.
-
On Relaxing Metric Information in Linear Temporal Logic
Authors:
Carlo A. Furia,
Paola Spoletini
Abstract:
Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but t…
▽ More
Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units.
△ Less
Submitted 17 June, 2011; v1 submitted 25 June, 2009;
originally announced June 2009.
