Requirements elicitation is still one of the most challenging activities of the requirements engineering process due to the difficulty requirements analysts face in understanding and translating complex needs into concrete requirements that directly impact the quality of the software to be developed.Although automated tools allow for assessing the syntactic quality of requirements, evaluating semantic metrics (e.g., language clarity, internal consistency) remains a manual and time-consuming activity.This paper explores how LLMs can help automate requirements elicitation within agile frameworks, where requirements are defined as user stories.We used 10 state-of-theart LLMs to investigate their ability to generate user stories automatically by emulating customer interviews.We evaluated the quality of user stories generated by LLMs, comparing it with the quality of user stories generated by humans (domain experts and students).We also explored whether and how LLMs can be used to automatically evaluate the semantic quality of user stories.Our results indicate that LLMs can generate user stories similar to humans in terms of coverage and stylistic quality, but exhibit lower diversity and creativity.Although LLMgenerated user stories are generally comparable in quality to those created by humans, they tend to meet the acceptance quality criteria less frequently, regardless of the scale of the LLM model.Finally, LLMs can reliably assess the semantic quality of user stories when provided with clear evaluation criteria and have the potential to reduce human effort in large-scale assessments.

The growing number of older adults facing isolation, cognitive decline, and technological exclusion poses critical challenges for the design of inclusive digital systems. Despite increasing research interest in age-inclusive technology, requirements engineering (RE) methods remain largely inadequate for this vulnerable population due to cognitive, linguistic, ethical, and contextual mismatches. This paper identifies four key challenges in applying RE to older adults: variability in cognitive and linguistic capabilities, ethical and privacy risks, fragmented design guidelines, and inconsistencies in requirements elicitation processes. To address these issues, we propose a multidisciplinary framework guided by artificial intelligence (AI) with five interlinked components: a community-driven corpus, age-sensitive elicitation techniques, emotionally intelligent tools for requirement creation, ethical awareness indicators, and inclusive validation processes. AI methods such as natural language processing, risk modeling, and adaptive interface analysis are embedded throughout the framework to personalize, automate, and validate RE processes for older adults. Our vision aims to foster technologies that are accessible, respectful, emotionally resonant, and practically effective for aging users, bridging the gap between RE research and real-world systems that empower older adults.

Formal methods for requirements engineering have existed for decades; yet, these techniques are rarely used if not required by certification because they are challenging for non-experts (e.g., novices and non-technical stakeholders in multidisciplinary teams) to interpret and apply. To enable non-experts to participate in collaborative software teams, we envision using artificial intelligence (AI) to assist in interpreting formal notations. Our research project investigates how and to what extent generative AI with large language models (LLMs) can be used to assist non-experts in interpreting formal requirements. In this paper, we conduct an exploratory investigation of both generating translations and interpreting linear temporal logic (LTL) formulae. Specifically, we explore prompting LLMs with sufficient information for the task of generating LTL formula explanations. With our initial prompt, we complete a classroom study where students learn LTL and then interpret a series of LTL formulae with and without the LLM-generated descriptions. We then improve our approach based on insights from the classroom study, and evaluate the overall quality of our updated prompt and the explanations it generates.

Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.

Large Language Models (LLMs) have made remarkable advancements in emulating human linguistic capabilities, showing potential also in executing various requirements engineering (RE) tasks. However, despite their generally good performance, the adoption of LLM-generated solutions and artefacts prompts concerns about their correctness, fairness, and trustworthiness. This paper aims to address the concerns associated with the use of LLMs in RE activities. Specifically, it seeks to develop a roadmap that leverages formal methods (FMs) to provide guarantees of correctness, fairness, and trustworthiness when LLMs are utilised in RE. Symmetrically, it aims to explore how LLMs can be employed to make FMs more accessible. We use two sets of examples to show the current limits of FMs when used in software development and of LLMs when used for RE tasks. The highlighted limitations are addressed by proposing two roadmaps grounded in the current literature and technologies. The proposed examples show the potential and limits of FMs in supporting software development and of LLMs when used for RE tasks. The initial investigation into how these limitations can be overcome has been concretised in two detailed roadmaps for the RE and, more largely, the software engineering community. The proposed roadmaps offer a promising approach to address the concerns of correctness, fairness, and trustworthiness associated with the use of LLMs in RE tasks through the use of FMs and to enhance the accessibility of FMs by utilising LLMs. • We exemplify the use of formal methods in software development • We outline a roadmap to increase usability of formal methods with the support of LLMs • We show how LLMs can be support requirements engineers in automating manual tasks • We propose a roadmap for the use of formal techniques to make LLMs reliable

Capturing users’ engagement is crucial for gathering feedback about the features of a software product. In a market-driven context, current approaches to collecting and analyzing users’ feedback are based on techniques leveraging information extracted from product reviews and social media. These approaches are hardly applicable in contexts where online feedback is limited, as for the majority of apps, and software in general. In such cases, companies need to resort to face-to-face interviews to get feedback on their products. In this article, we propose to utilize biometric data, in terms of physiological and voice features, to complement product feedback interviews with information about the engagement of the user on 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 biofeedback and voice data, and that voice features alone can be sufficiently effective. The best configurations evaluated achieve an average F1 ∼ 70% in terms of classification performance, and use voice features only. This work is one of the first studies in requirements engineering in which biometrics are used to identify emotions. Furthermore, this is one of the first studies in software engineering that considers voice analysis. The usage of voice features can be particularly helpful for emotion-aware feedback collection 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.

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 empirically analyse this technique in a realistic scenario, in which it is used to extend the requirements of a product that were initially captured by means of more traditional requirements elicitation interviews. Considering this scenario, we conduct an experimental simulation with 58 analysts and collect qualitative data. We perform thematic analysis of the data to identify strategies, benefits, and challenges of app store-inspired elicitation, as well as differences with respect to interviews in the considered elicitation setting. 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 fostering app store-inspired elicitation among practitioners.

Abstract Requirements are elicited from the customer and other stakeholders through an iterative process of interviews, prototyping, 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. The rest of the content is dedicated to new requirements, and up to 21% of it belongs to completely novel topics. 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.

Privacy requirements have become increasingly important as information about us is continuously accumulated and digitally stored. However, despite the many proposed methodologies and tools to address these requirements, privacy engineering is often underperformed in most domains of the software industry. Two of the major reasons underlying this under-performance are (1) the low expertise and understanding of privacy by the two main actors in requirements engineering: users and analysts, and (2) the fact that software developers often do not perceive privacy requirements as a priority for their companies, thus neglecting to meet these requirements even when they do have the required knowledge, skills, and supporting tools to do so. To address these two problems, we propose to integrate knowledge from software engineering and organizational psychology in an iterative, customizable, socio-technical environment. Such environment has the potential to support the design of systems by providing technical tools for eliciting, modeling, and designing privacy aspects, thus addressing the knowledge gap of both data subjects and analysts, and social mechanisms for achieving a supportive and sustainable organizational privacy climate within a company, thus reorienting the organizational attention and engagement toward addressing privacy requirements.

Requirements are elicited from the customer and other stakeholders through an iterative process of interviews, prototyping, and other interactive sessions. Many communication phenomena may emerge in these early iterations, that lead initial ideas to be transformed, renegotiated, or reframed. Understanding how this process takes place can help in solving possible communication issues as well as their consequences. In this work, we perform an exploratory study of descriptive nature to understand in which way requirements get transformed from initial ideas into documented needs. To this end, we select 30 subjects that act as requirements analysts, and we perform a set of elicitation sessions with a fictional customer. The customer is required to study a sample requirements document for a system beforehand and to answer the questions of the analysts about the system. After the elicitation sessions, the analysts produce user stories for the system. These are compared with the original ones by two researchers to assess to which extent and in which way the initial requirements evolved throughout the interactive sessions. Our results show that between 30% and 38% of the produced user stories include content that can be fully traced to the initial ones, while the rest of the content is dedicated to new requirements. We also show what types of requirements are introduced through the elicitation process, and how they vary depending on the analyst. Our work contributes to theory in requirements engineering, with empirically grounded, quantitative data, concerning the impact of elicitation activities with respect to initial ideas.

Abstract Model design is not a linear, one-shot process. It proceeds through refinements and revisions. To effectively support developers in generating model refinements and revisions, it is desirable to have some automated support to verify evolvable models. To address this problem, we recently proposed to adopttopological proofs, which are slices of the original model that witness property satisfaction. We implemented TOrPEDO, a framework that provides automated support for using topological proofs during model design. Our results showed that topological proofs are significantly smaller than the original models, and that, in most of the cases, they allow the property to be re-verified by relying only on a simple syntactic check. However, our results also show that the procedure that computes topological proofs, which requires extracting unsatisfiable cores of LTL formulae, is computationally expensive. For this reason, TOrPEDO currently handles models with a small dimension. With the intent of providing practical and efficient support for flexible model design and wider adoption of our framework, in this paper, we propose an enhanced—re-engineered—version of TOrPEDO. The new version of TOrPEDO relies on anovelprocedure to extract topological proofs, which has so far represented the bottleneck of TOrPEDO performances. We implemented our procedure within TOrPEDO by considering Partial Kripke Structures (PKSs) and Linear-time Temporal Logic (LTL): two widely used formalisms to express models with uncertain parts and their properties. To extract topological proofs, the new version of TOrPEDO converts the LTL formulae into an SMT instance and reuses an existing SMT solver (e.g., Microsoft Z3) to compute an unsatisfiable core. Then, the unsatisfiable core returned by the SMT solver is automatically processed to generate the topological proof. We evaluated TOrPEDO by assessing (i) how does the size of the proofs generated by TOrPEDO compares to the size of the models being analyzed; and (ii) how frequently the use of the topological proof returned by TOrPEDO avoids re-executing the model checker. Our results show that TOrPEDO provides proofs that are smaller ( ≈ 60%) than their respective initial models effectively supporting designers in creating model revisions. In a significant number of cases ( ≈ 79%), the topological proofs returned by TOrPEDO enable assessing the property satisfaction without re-running the model checker. We evaluated our new version of TOrPEDO by assessing (i) how it compares to the previous one; and (ii) how useful it is in supporting the evaluation of alternative design choices of (small) model instances in applied domains. The results show that the new version of TOrPEDO is significantly more efficient than the previous one and can compute topological proofs for models with less than 40 states within two hours. The topological proofs and counterexamples provided by TOrPEDO are useful to support the development of alternative design choices of (small) model instances in applied domains.

The core aim of requirements inspection is to ensure the high quality of already elicited requirements in the Software Requirements Specification. Teaching requirements inspection to novices is challenging, as inspecting requirements needs several skills as well as knowledge of the product and process that is hard to achieve in a classroom environment. Published studies about pedagogical design specifically for teaching requirements inspection are scarce. Our objective is to present the design and evaluation of a postgraduate course for requirements inspection training. We conducted an empirical study with 138 postgraduate students, teamed up in 34 groups to conduct requirements inspection. We performed qualitative analysis on the data collected from students' reflection reports to assess the effects of the pedagogical design in terms of benefits and challenges. We also quantitatively analyze the correlation between the students' performance in conducting inspections and their ability of writing specifications. From the analysis of students' reflections, several themes emerged such as their difficulty of working with limited information, but also revealed the benefits of learning teamwork and writing good requirements. This qualitative analysis also provides recommendations for improving the related activities. The results revealed a moderate positive correlation between the performance in writing specification and inspection.

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 biofeedback to complement interviews with information about the engagement of the user on the discussed features and topics. We evaluate our approach by interviewing users while gathering their biometric data using an Empatica E4 wristband. Our results show that we can predict users' engagement by training supervised machine learning algorithms on the biometric data. The results of our work can be used to facilitate the prioritization of product features and to guide the interview based on users' engagement.

Interviews are largely used in the practice of requirements elicitation. Nevertheless, performing an effective interview often depends on soft-skills, and on knowledge acquired through experience. When it comes to requirements engineering education and training (REET), limited resources and few well-founded pedagogical approaches are available to allow students to acquire and improve their skills as interviewers. This paper presents a novel pedagogical approach that combines role-playing, peer-review and self-assessment to enable students to reflect on their mistakes, and improve their interview skills. We evaluate the approach through a controlled quasi-experiment. The study shows that the approach significantly reduces the amount of mistakes made by the students. Feedback from the participants confirms the usefulness and easiness of the proposed training. This work contributes to the body of knowledge of REET with an empirically evaluated method for teaching inter-views. Furthermore, we share the pedagogical material used, to enable other educators to apply and possibly tailor the approach.

Abstract Controllers often are large and complex reactive software systems and thus they typically cannot be developed as monolithic products. Instead, they are usually comprised of multiple components that interact to provide the desired functionality. Components themselves can be complex and in turn be decomposed into multiple sub-components. Designing such systems is complicated and must follow systematic approaches, based on recursive decomposition strategies that yield a modular structure. This paper proposes FIDDle–a comprehensive verification-driven framework which provides support for designers during development. FIDDle supports hierarchical decomposition of components into sub-components through formal specification in terms of pre- and post-conditions as well as independent development, reuse and verification of sub-components. The framework allows the development of an initial, partially specified design of the controller, in which certain components, yet to be defined, are precisely identified. These components can be associated with pre- and post-conditions, i.e., a contract, that can be distributed to third-party developers. The framework ensures that if the components are compliant with their contracts, they can be safely integrated into the initial partial design without additional rework. As a result, FIDDle supports an iterative design process and guarantees correctness of the system at any step of development. We evaluated the effectiveness of FIDDle in supporting an iterative and incremental development of components using the K9 Mars Rover example developed at NASA Ames. This can be considered as an initial, yet substantive, validation of the approach in a realistic setting. We also assessed the scalability of FIDDle by comparing its efficiency with the classical model checkers implemented within the LTSA toolset. Results show that FIDDle scales as well as classical model checking as the number of the states of the components under development and their environments grow.

Software systems are usually formed by multiple components which interact with one another. In large systems, components themselves can be complex systems that need to be decomposed into multiple sub-components. Hence, system design must follow a systematic approach, based on a recursive decomposition strategy. This paper proposes a comprehensive verification-driven framework which provides support for designers during development. The framework supports hierarchical decomposition of components into sub-components through formal specification in terms of pre- and post-conditions as well as independent development, reuse and verification of sub-components.

Software engineering is inherently a human-centric and collaborative process and this reflects in its teaching programs, as most of the courses comprise projects and team efforts. In order to fairly evaluate students, there is the problem of quantifying the amount of work contributed to the team development project by each of its members. Most commonly, in order to estimates student contributions, instructors use arbitrary and subjective judgment derived from observations and evaluations. The currently used process is not a complete picture and is time consuming since it requires numerous observations and extensive paperwork's review. Emerging decentralized systems (such as git) and their widespread applications in all realms of development which capitalize on team-aware metrics, are worthwhile and can provide a solution to the problem. In this work we support a solution that utilizes git-driven technology, and its related features, to measure a team member's contributions objectively, based not only upon the completion of the project, but also at any time during progression development. Such performance assessment could generate more productive team-based learning with higher-quality graduates for better meeting software industry's expectations.

This innovative practice work in progress paper tackles the problem of unfairness and bias in software, that recently has emerged in countless cases. This unfairness can be present in the way software makes its decision or can limit the software functionalities to work only with certain populations. Well-known examples of this problem are the Microsoft Kinect facial recognition algorithm, which does not work properly with darker skin players, and the software used in 2016 by Amazon.com to determine the parts of the United States to which offer free same-day delivery that made decisions that prevented minority neighborhoods from participating in the program. The reasons behind these phenomena have often roots in the fact that software is created by humans who are biased and live in biased and non-inclusive environments. Recent research from the software engineering community is starting to tackle this problem at many levels from requirements analysis to the new automatic fairness testing technique (proposed first at FSE 2017 conference). However, research in bias of software is still a very undervalued and rarely discussed problem as software is often seen as a product immune to bias and non-inclusivity. This problem will be not addressed unless software engineering educators start to include this notion as a first-class problem in their foundation courses to future generation of scholars. In this work, we propose a set of bias-aware guidelines and taxonomy on how to flesh out this problem and possible solutions to it in software engineering curricula.

[Context] Interviews are the most widely used elicitation technique in requirements engineering. However, conducting effective requirements elicitation interviews is challenging, due to the combination of technical and soft skills that requirements analysts often acquire after a long period of professional practice. Empirical evidence about training the novices on conducting effective requirements elicitation interviews is scarce. [Objectives] We present a list of most common mistakes that novices make in requirements elicitation interviews. The objective is to assist the educators in teaching interviewing skills to student analysts. [Re-search Method] We conducted an empirical study involving role-playing and authentic assessment with 110 students, teamed up in 28 groups, to conduct interviews with a customer. One re-searcher made observation notes during the interview while two researchers reviewed the recordings. We qualitatively analyzed the data to identify the themes and classify the mistakes. [Results and conclusion] We identified 34 unique mistakes classified into 7 high level themes. We also give examples of the mistakes made by the novices in each theme, to assist the educationists and trainers. Our research design is a novel combination of well-known pedagogical approaches described in sufficient details to make it re-peatable for future requirements engineering education and training research.

Modern Building Management Systems (BMSs) have been designed to automate the behavior of complex buildings, but unfortunately they do not allow occupants to customize it according to their preferences, and only the facility manager is in charge of setting the building policies. To overcome this limitation, we present BuildingRules, a trigger-action programming-based system that aims to provide occupants of commercial buildings with the possibility of specifying the characteristics of their office environment through an intuitive interface. Trigger-action programming is intuitive to use and has been shown to be effective in meeting user requirements in home environments. To extend this intuitive interface to commercial buildings, an essential step is to manage the system scalability as large number of users will express their policies. BuildingRules has been designed to scale well for large commercial buildings as it automatically detects conflicts that occur among user specified policies and it supports intelligent grouping of rules to simplify the policies across large numbers of rooms. We ensure the conflict resolution is fast for a fluid user experience by using the Z3 SMT solver. BuildingRules backend is based on RESTful web services so it can connect to various BMSs and scale well with large number of buildings. We have tested our system with 23 users across 17 days in a virtual office building, and the results we have collected prove the effectiveness and the scalability of BuildingRules.

The requirements elicitation process often starts with an interview between a customer and a requirements analyst. During these interviews, ambiguities in the dialogic discourse may reveal the presence of tacit knowledge that needs to be made explicit. It is therefore important to understand the nature of ambiguities in interviews and to provide analysts with cognitive tools to identify and alleviate ambiguities. Ambiguities perceived by analysts are sometimes triggered by specific categories of terms used by the customer such as pronouns, quantifiers, and vague or under-specified terms. However, many of the ambiguities that arise in practice cannot be rooted in single terms. Rather, entire fragments of speech and their relation to the mental state of the analyst need to be considered.In this paper, we show that particular types of ambiguities can be characterised by means of argumentation theory. Argumentation is the study of how conclusions can be reached through logical reasoning. In an argumentation theory, statements are represented as arguments, and conflict relations among statements are represented as attacks. Based on a set of ambiguous fragments extracted from interviews, we define a model of the mental state of the analyst during an interview and translate it into an argumentation theory. Then, we show that many of the ambiguities can be characterized in terms of 'attacks' on arguments. The main novelty of this work is in addressing the problem of explaining fragment-level ambiguities in requirements elicitation interviews through the formal modeling of the analyst's mental model using argumentation theory. Our contribution provides a data-grounded, theoretical basis to have a more complete understanding of the ambiguity phenomenon, and lays the foundations to design intelligent computer-based agents that are able to automatically identify ambiguities.

In requirements elicitation interviews, ambiguities identified by analysts can help to disclose the tacit knowledge of customers. Indeed, ambiguities might reveal implicit or hard to express information that needs to be elicited. The perception of ambiguity might depend on the subject who is acting as analyst, and different analysts might identify different ambiguities in the same interview. Based on this intuition, we propose to investigate the difference between ambiguities explicitly revealed by an analyst during a requirements elicitation interview, and ambiguities annotated by a reviewer who listens to the interview recording, with the objective of defining a method for interview review. We performed an exploratory study in which two subjects listened to a set of customer-analyst interviews. Only in 26% of the cases the ambiguities revealed by the analysts matched with the ambiguities found by the reviewers. In 46% of the cases, ambiguities were found by the reviewers, and were not detected by the analysts. Based on these preliminary findings, we are currently performing a controlled experiment with students of two universities, which will be followed by a real-world case study with companies. This paper discusses the current results, together with our research plan.

Requirements elicitation is the initial step of the requirements engineering process and aims at gathering all the relevant requirements through the direct or indirect interactions between requirements analysts and stakeholders. Even if the requirements elicitation problem is not new and has been approached many times over the years, it is still considered one of the most challenging of the requirements engineering process. In the proposed presentation, we aim at analyzing the journey of the research on requirements elicitation through the 25 years of the Requirements Engineering conference not only by considering the different proposed approaches and their evolution, but also by evaluating the role of requirements elicitation in the conference. Moreover, we will present the lessons learnt during this analysis and will use them as a starting point to present the current trends and outline possible future directions.

Customer-analyst interviews are considered among the most effective means to perform requirements elicitation. However, during these interviews, ambiguity can hamper communication between customer and requirements analyst. Ambiguity is particularly dangerous in those cases in which the analyst misunderstands some linguistic expression of the customer, with-out being aware of the misunderstanding. On the other hand, if the analyst is able to detect ambiguous situations, this has been shown to help him/her in disclosing tacit knowledge. Indeed, the occurrence of an ambiguity might reveal the presence of unexpressed, system-relevant knowledge that needs to be elicited. Therefore, for the requirements elicitation interview to succeed, it is important for the analyst not to overlook ambiguities. To support the ambiguity-awareness of the requirements analyst, this paper aims to provide a set of cues that can be identified in the linguistic expressions of the customer, and that typically lead to ambiguity. To this end, we performed 34 customer-analyst interviews, and we isolated the speech fragments that caused the ambiguity. Based on the analysis of these fragments, and leveraging the previous literature on ambiguity in written requirements, we identified a set of cues that can be used by requirements analysts as a reference handbook to detect ambiguities.

Interviews with stakeholders are the most commonly used elicitation technique, as they are considered one of the most effective ways to transfer knowledge between requirements analysts and customers. During these interviews, ambiguity is a major obstacle for knowledge transfer, as it can lead to incorrectly understood needs and domain aspects and may ultimately result in poorly defined requirements. To address this issue, previous work focused on how ambiguity is perceived on the analyst side, i.e., when the analyst perceives an expression of the customer as ambiguous. However, this work did not consider how ambiguity can affect customers, i.e., when questions from the analyst are perceived as ambiguous. Since customers are not in general trained to cope with ambiguity, it is important to provide analysts with techniques that can help them to identify these situations. To support the analysts in this task, we propose to explore the relation between a perceived ambiguity on the customer side, and changes in the voice and bio parameters of that customer. To realize our idea, we plan to (1) study how changes in the voice and bio parameters can be correlated to the levels of stress, confusion, and uncertainty of an interviewee and, ultimately, to ambiguity and (2) investigate the application of modern voice analyzers and wristbands in the context of customer-analyst interviews. To show the feasibility of the idea, in this paper we present the result of our first step in this direction:an overview of different voice analyzers and wristbands that can collect bio parameters and their application in similar contexts. Moreover, we propose a plan to carry our research out.

Interviews are the most common and effective means to perform requirements elicitation and support knowledge transfer between a customer and a requirements analyst. Ambiguity in communication is often perceived as a major obstacle for knowledge transfer, which could lead to unclear and incomplete requirements documents. In this paper, we analyse the role of ambiguity in requirements elicitation interviews. To this end, we have performed a set of customer-analyst interviews to observe how ambiguity occurs during requirements elicitation. From this direct experience, we have observed that ambiguity is a multi-dimensional cognitive phenomenon with a dominant pragmatic facet, and we have defined a phenomenological framework to describe the different types of ambiguity in interviews. We have also discovered that, rather than an obstacle, the occurrence of an ambiguity is often a resource for discovering tacit knowledge. Starting from this observation, we have envisioned the further steps needed in the research to exploit these findings.

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.

In the past years, the adoption of adaptive systems has increased in many fields of computer science, such as databases and software engineering. These systems are able to automatically react to events by collecting information from the external environment and generating new events. However, the collection of data is often hampered by uncertainty and vagueness. The decision-making mechanism used to produce a reaction is also imprecise and cannot be evaluated in a crisp way, as it depends on vague temporal constraints expressed by humans. Logic has been extensively used as an abstraction to express vagueness in the satisfaction of system properties, as well as to enrich existing modeling formalisms. However, existing attempts to fuzzify the temporal modalities still have some limitations. Existing fuzzy temporal languages are generally obtained from classical temporal logic by replacing classical connectives or propositions with their fuzzy counterparts. Hence, these languages do not allow us to represent temporal properties, such as “almost always” and “soon,” in which the notion of time is inherently fuzzy. To overcome these limitations, we propose a temporal framework, fuzzy-time temporal logic (FTL), to express vagueness on time. This framework formally defines a set of fuzzy temporal modalities that 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 mutual relations. We also prove that under the assumption that all events are crisp, FTL reduces to linear temporal logic (LTL). Moreover, 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 of the other ones.

Modern software systems are often characterized by uncertainty and changes in the environment in which they are embedded. Hence, they must be designed as adaptive systems. We propose a framework that supports adaptation to non-functional manifestations of uncertainty. Our framework allows engineers to derive, from an initial model of the system, a finite state automaton augmented with probabilities. The system is then executed by an interpreter that navigates the automaton and invokes the component implementations associated to the states it traverses. The interpreter adapts the execution by choosing among alternative possible paths of the automaton in order to maximize the system's ability to meet its non-functional requirements. To demonstrate the adaptation capabilities of the proposed approach we implemented an adaptive application inspired by an existing worldwide distributed mobile application and we discussed several adaptation scenarios.

Conventional formal verification techniques rely on the assumption that a system's specification is completely available so that the analysis can say whether or not a set of properties will be satisfied. On the contrary, modern development lifecycles call for agileincremental and iterativeapproaches to tame the boosting complexity of modern software systems and reduce development risks. We focus here on requirements verification performed in the early exploratory stages on high-level models and we discuss how this can be integrated into an agile approach. We present a new technique to model-check incomplete high-level specifications against formally specified requirements. We do this in the context of incomplete hierarchical Statecharts, verified against a variation of CTL properties. Our approach supports step-wise specification and refinement verification. Verification can be incremental, that is alternative refinements may be separately explored and verification is only replayed for the modified parts. The results are presented by introducing the formalisms, the model-checking algorithm, and the tool we have implemented.

A model has variability bounded by v/k when the state changes at most v times over any linear interval containing k time instants. When interpreted over models with bounded variability, specification formulae that contain redundant metric information -- through the usage of next operators -- can be simplified without affecting their validity. This paper shows how to harness this simplification in practice: we present a translation of LTL into Büchi automata that removes redundant metric information, hence makes for more efficient verification over models with bounded variability. To show the feasibility of the approach, we also implement a proof-of-concept translation in ProMeLa and verify it using the Spin off-the-shelf model-checker.

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.

Self-adaptation is imposing as a key characteristic of many modern software systems to tackle their complexity and cope with the many environments in which they can operate. Self-adaptation is a requirement per-se, but it also impacts the other (conventional) requirements of the system; all these new and old requirements must be elicited and represented in a coherent and homogenous way. This paper presents FLAGS, an innovative goal model that generalizes the KAOS model, adds adaptive goals to embed adaptation countermeasures, and fosters self-adaptation by considering requirements as live, runtime entities. FLAGS also distinguishes between crisp goals, whose satisfaction is boolean, and fuzzy goals, whose satisfaction is represented through fuzzy constraints. Adaptation countermeasures are triggered by violated goals and the goal model is modified accordingly to maintain a coherent view of the system and enforce adaptation directives on the running system. The main elements of the approach are demonstrated through an example application.

The research described in this paper shows how the runtime relocation of a reconfigurable component can be obtained using a system component that is able to update the bitstream information, moving the reconfigurable module in the desired position. This scenario defines the so-called partial bitstream relocation activity. This paper proposes a relocation filter that can be implemented both as a hardware and a software component. The former is hosted in the static part of the reconfigurable architecture, while the latter is made to be run on the processor placed on the field-programmable gate array (FPGA). The proposed approach has also been validated over different FPGAs, i.e., Virtex II Pro, Virtex 4, and Virtex 5, proposing a runtime relocation support that can be customized to meet all the different constraints associated with these different target architectures.

Web service based applications are expected to live in dynamically evolving settings. At run-time, services may undergo changes that could modify their expected behavior. Because of such intrinsic dynamic nature, applications should be designed by adhering to the principles of design- by-contract. Run-time monitoring is needed to check that the contract between service providers and service users is fulfilled while the collaboration is in place. We describe a language to specify the expected functional and non-functional requirements that a service provider should fulfill. The language (timed WSCoL) is a temporal extension of a previous proposal (WSCoL). We also illustrate the architecture of a run-time analyzer that checks timed WSCoL properties. Should such properties be disproved during execution, appropriate recovery and reconfiguration actions may be put in place.

Designing systems mapped onto FPGAs that foresee a dynamic reconfiguration of the application is a difficult task. It requires that the identification of the reconfigurable tasks and their allocation onto the FPGA must be defined during the design phases. Furthermore, also the schedule of dynamic reconfigurations must be defined. This paper presents an improved scheduling and allocation of reconfigurable tasks onto an FPGA, based on the coloring problem. The proposed algorithm stems from the one previously presented (Ferrandi et al., 2005), but introduces backtracking to improve the performance in terms of number of number of colors, that represent FPGAs areas. The new algorithm has been experimented on the Xilinx-based architecture defined to support dynamic reconfigurability (Donato et al., 2005)

The need of formal verification is a problem that involves all the fields in which sensible data are managed. In this context the verification of data streams became a fundamental task. The purpose of this paper is to present a framework, based on the model checker SPIN, for the verification of data streams.The proposed method uses a linear temporal logic, called TRIO, to describe data constraints and properties. Constraints are automatically translated into Promela, the input language of the model checker SPIN in order to verify them.