Abstract Requirements Engineering (RE) is a socio-technical process that relies on effective communication among stakeholders. Understanding how national cultural influences affect RE activities is crucial, given participants’ diverse cultural backgrounds. This paper presents a refined framework for identifying cultural influences (CIs) on RE-related activities and a web-based application developed to support it. The refined framework incorporates the latest Hofstede scores and covers nearly double the CIs compared to its earlier version. We evaluated the proposed framework against in-depth case studies from 8 countries (Australia, Thailand, China, Pakistan, South Korea, Saudi Arabia, Vietnam, and Bangladesh), where the CIs have been identified on the basis of surveys and interviews. Analysis showed the proposed framework consistently provided better coverage than the original. We extended the framework by assigning evidence-based confidence levels to each CIs based on the evaluation wrt. primary case studies. Our approach allows RE practitioners to evaluate and manage cultural impacts effectively. The framework provides a comprehensive analysis of national cultural influences and delivers more accurate and contextually relevant insights. The tool aids users in obtaining relevant national CIs, confidence levels, and summaries for a selected country. This enables stakeholders, practitioners, researchers, and educators to manage cultural dynamics effectively, enhancing RE-related activities.

Requirements Engineering (RE) is one of the most interaction-intensive phases of software development. This means that RE activities might be especially impacted by stakeholders’ national culture. Software development projects increasingly have a very diverse range of stakeholders. To future-proof RE activities, we need to help RE practitioners avoid misunderstandings and conflicts that might arise from not understanding potential Cultural Influences (CIs). Moreover, an awareness of CIs supports diversity and inclusion in the IT profession. Bangladesh has a growing IT sector with some unique socio-cultural characteristics, and has been largely overlooked in this research field. In this study, we aim to investigate how the RE process is adopted in the context of Bangladeshi culture and what cultural influences impact overall RE activities.

Metamorphic testing (MT) is a general approach for the testing of a specific kind of software systems – so-called “non-testable”, where the “classical” testing approaches are difficult to apply. MT is an effective approach for addressing the test oracle problem and test case generation problem. The test oracle problem is when it is difficult to determine the correct expected output of a particular test case or to determine whether the actual outputs agree with the expected outcomes. The core concept in MT is metamorphic relations (MRs) which provide formal specification of the system under test. One of the challenges in MT is effective test generation. Property-based testing (PBT) is a testing methodology in which test cases are generated according to desired properties of the software. In some sense, MT can be seen as a very specific kind of PBT. In this paper, we show how to use PBT tools to automate test generation and verification of MT. In addition to automation benefit, the pro posed method shows how to combine general PBT with MT under the same testing framework.

Requirement Engineering (RE) is a socio-technical activity and it demands intensive communication with the stake-holders to elicit and model all requirements. As both national and organisational cultures influence the behaviour of the individuals and their work practices, they might also influence RE activities deeply. We propose an extension to a formal framework for identifying and analysing cultural influences that could impact RE activities: the aim is to apply the framework not only on the national culture level, but expand it to the level of organisational culture to provide a more nuanced approach.

Requirements Engineering (RE) activities require intensive communication to capture clients' requirements. As culture influences the way in which people communicate and interact, individuals' culture might influence the implementation of RE activities. In this paper, we discuss the differences between formal approach (using the framework we propose) and case-study-based approaches for the identification of cultural influences in RE. We compared the results of the application of our framework with the results of case studies conducted by other researchers from several cultures. The results showed that the framework provided a much higher degree of precision than expected: the framework identified almost all of the cultural influences mentioned in the identified cases studies. This provides evidence of the accuracy and validity of our framework, which can provide similar conclusions based on information about the cultures involved rather than in-depth analysis.

Requirements Engineering (RE) is a critical process in the development of any software. It requires intensive communication among many stakeholders in order to identify software requirements accurately. As RE activities require intensive communication, cultural influences might need to be considered to improve these activities and to avoid issues that might affect the software project outcomes. In our work, we explored the influence of national culture on RE activities. We conducted an empirical study in two countries that have different cultural profiles: Saudi Arabia and Australia. To explore this issue, we conducted 41 face-to-face interviews. To consolidate the collected data, we conducted also 30 follow-up interviews with the same practitioners. The aim of our study was to empirically identify the set of cultural influences affecting RE activities, and analyse their implication on RE activities. This paper reports the results of the analysis of participants’ responses with respect to their industrial profiles, in terms of three factors: the type of software methodology applied by the participants (Traditional vs. Agile), the size of their company/organisation (small, medium, and large), and its type (private vs. government). The results showed a number of significant differences in the cultural influences that determine the type of software development methodology, i.e., Traditional or Agile, being applied within the corresponding company. In this paper, we discuss the identified differences and the factors that determine them. This in-depth analysis provides a broader examination of the influence of culture on RE activities, which might assist RE practitioners to select the most suitable RE practices/methodology to overcome any negative effects of these influences.

Requirements Engineering (RE) activities require intensive communication among different stakeholders and an understanding of their behaviour in order to accurately identify requirements. As RE requires intensive communication, an individual's culture might influence RE activities. Thus, cultural influences affecting RE activities might need to be considered to improve RE activities and prevent issues that might affect software project outcomes. In our work, we propose a framework for identifying cultural factors that could influence RE activities. In this paper, we present the preliminary results of a case study conducted with Vietnamese practitioners.

Requirements Engineering (RE) activities are inherently collaborative, requiring software stakeholders to have intensive communication to identify users’ requirements. As the stakeholders’ culture might heavily impact on the way how they collaborate and communicate, RE might be significantly influenced by their cultural background. To analyse stakeholders’ culture, we use one of the most adopt and comprehensive cultural studies in software engineering: Hofstede’s cultural model. Hofstede’s model has six cultural dimensions, where one of them is Power Distance (PD). The aim of this study is to explore the influence of PD cultural aspects on RE activities. We conducted 32 interviews with software developments/requirements engineer practitioners from two different cultures: Saudi Arabia and Australia. Our results revealed that PD significantly affect RE collaboration among software stakeholders. In this paper, we address the core identified cultural aspects as well as the ways to overcome them. The results that we present in this paper would help to increase awareness of the influence of PD, and thus, improve collaboration within RE activities.

Software development requires intensive communication between the requirements engineers and software stakeholders, particularly during the Requirements Engineering (RE) phase. Therefore, the individuals' culture might influence both the RE process and the result. Our aims are to investigate the extend of cultural influences on the RE process, and to analyze how the RE process can be adapted to take into account cultural aspects. The model we present is based on Hofstede's cultural theory. The model was applied on a pilot case study in the context of the conservative Saudi Arabian culture. The results reveal 6 RE aspects and 10 cultural factors that have a large impact on the RE practice.

The Requirements Engineering (RE) process is crucial for identifying users' requirements and the success of the software development process. As RE is a socio-technical activity in nature, an individuals' culture might influence its activities deeply. The aim of this study is to observe and evaluate the influence of culture on the RE process. In total, we conducted 16 interviews with requirements engineer practitioners in Saudi Arabia and Australia. We found that both cultures have an impact on the RE process. This paper describes the lessons learned from practice on how to improve RE practices, taking into account cultural aspects.

Player Modelling is one of the challenges in Interactive Narratives (INs), where a precise representation of the players mental state is needed to provide a personalised experience. However, how to represent the interaction of the player with the game to make the appropriate decision in the story is still an open question. In this paper, we aim to bridge this gap identifying the information needed to capture the players interaction with an IN using the Belief-Desire-Intention (BDI) model of agency. We present a BDI design to mimic a players interaction with a simplified version of the interactive fiction Anchorhead.

We aim to facilitate semi-automated collaborative distributed development, commissioning, operation and maintenance using formal behavioural models. We are interested in a whole-of-system context, where properties of the physical systems increasingly depend explicitly on software configuration, thus requiring validation. Our models are cyber-physical, comprising not only the control software itself but also mechatronic elements under control involving sensing/actuators, such as pneumatics, hydraulics, and motor drives. We discuss various issues relevant to the problems of collaboration, and we provide requirements for collaboration in a specific experimental context involving elements of a small-scale food packaging plant.

Agent systems are used for a wide range of applications, and techniques to detect and avoid defects in such systems are valuable. In particular, it is desirable to detect issues as early as possible in the software development lifecycle. We describe a technique for checking the plan structures of a BDI agent design against the requirements models, specified in terms of scenarios and goals. This approach is applicable at design time, not requiring source code. A lightweight evaluation demonstrates that a range of defects can be found using this technique.

Given the current set of intentions an autonomous agent may have, intention selection is the agent's decision which intention it should focus on next. Often, in the presence of conflicts, the agent has to choose between multiple intentions. One factor that may play a role in this deliberation is the level of completeness of the intentions. To that end, this paper provides pragmatic but principled mechanisms for quantifying the level of completeness of goals in a BDI-style agent. Our approach leverages previous work on resource and effects summarization but we go beyond by accommodating both dynamic resource summaries and goal effects, while also allowing a non-binary quantification of goal completeness. We demonstrate the computational approach on an autonomous robot case study.

Intelligent agent systems are often used to implement complex software systems. A key aspect of agent systems is goals: a programmer or user defines a set of goals for an agent, and then the agent is left to determine how best to satisfy the goals assigned to it. Such goals include both achievement goals and maintenance goals. An achievement goal describes a particular state the agent would like to become true, such as being in a particular location or having a particular bank balance. A maintenance goal specifies a condition which is to be kept satisfied, such as ensuring that a vehicle stays below a certain speed, or that it has sufficient fuel. Current agent systems usually only utilize reactive maintenance goals, in that the agent only takes action after the maintenance condition has been violated. In this paper, we discuss methods by which maintenance goals can be made proactive, i.e., acting before a maintenance condition is violated, having predicted that the maintenance condition will be violated in the future. We provide a representation of proactive maintenance goals, reasoning algorithms, an operational semantics that realizes these algorithms and an experimental evaluation of our approach.

Proof search in inference systems such as the sequent calculus is a process of discovery. Once a proof is found, there is often information in the proof which is redundant. In this article we show how to detect and eliminate certain kinds of redundant formulae from a given proof, and in particular in a way which does not require further proof search or any rearrangement of the proof found. Our technique involves adding constraints to the inference rules, which are used once the proof is complete to determine redundant formulae and how they may be eliminated. We show how this technique can be applied to propositional linear logic, and prove its correctness for this logic. We also discuss how our approach can be extended to other logics without much change.

This paper describes the development of a classification scheme that can be used to investigate the characteristics of introductory programming examinations. We describe the process of developing the scheme, explain its categories, and present a taste of the results of a pilot analysis of a set of CS1 exam papers. This study is part of a project that aims to investigate the nature and composition of formal examination instruments used in the summative assessment of introductory programming students, and the pedagogical intentions of the educators who construct these instruments.

Agent systems based on the BDI paradigm need to make decisions about which plans are used to achieve their goals. Usually the choice of which plan to use to achieve a particular goal is left up to the system to determine. In this paper we show how preferences, which can be set by the user of the system, can be incorporated into the BDI execution process and used to guide the choices made.

Introduction. Deliberation over courses of action to pursue is fundamental to agent systems. Agents designed to work in dynamic environments, such as a rescue robot or an online travel agent, must be able to reason about what actions they should take, incorporating deliberation into their execution cycle, reviewing decisions and taking corrective action with appropriate focus and frequency. Not only must agents reason about the effects of their courses of action, they must also consider the semantics of these corrective actions. Systems based on the well-known Belief-Desire-Intention (BDI) framework most often ascribe a set of goals to the agent, which is equipped with various techniques to deliberate over and manage this set. The centrality of reasoning over goals is seen in the techniques investigated in the literature, which include subgoaling and plan selection, detection and resolution of conflicts or opportunities for cooperation [9], checking goal properties to specification [10, 5], failure recovery and planning [2], and dropping, aborting, or suspending and resuming goals [7]. A variety of goals are described in the literature, including goals of performance of a task, achievement of a state, querying truth of a statement, testing veracity of beliefs, and maintenance of a condition [1, 11]. An agent must manage such a variety of goals, while incorporating pertinent sources of information into its decisions over them, such as preferences, quality goals, motivational goals, and advice [10]. The complexity of agent goal management stems from this combination of the variety of goals and the breadth of deliberation considerations. It is furthered because each goal can be dropped, aborted, suspended, or resumed (as illustrated in Figure 1) at arbitrary times. While goals themselves are static (i.e., they are specified at design time, and do not change during execution), their behaviour is dynamic: a goal may undergo a variety of changes of state during its execution cycle [5]. This evolution may include its initial adoption by the agent, being actively pursued, being suspended and then later resumed, and eventually succeeding (or failing). (Maintenance goals have a subtle life-cycle: the goal is retained even when the desired property is true; it is possible that such goals are never dropped.) Our work analyzes the behaviour of the above types of goals, including the behaviour when goals are aborted or suspended. We consider the complete life-cycle of goals, from their initial adoption by the agent to the time when they are no longer of interest, and all stages in between; we account for the dynamics of plan execution and sub-goaling. We develop a generic framework for goal states and transitions that captures the life-cycle of goals—shown in summary in Figure 1; the Active and Suspended states decomposed further [8]—

It is well-known that proof search, in general, does not terminate. In some decidable logics (e.g. intuitionistic propositional logic) it is possible to give a terminating sequent calculus, i.e. one in which a naive backward proof search will always terminate. However, such calculi are not always available, even for decidable logics. In this paper we investigate the incorporation of a loop detection mechanism into an inference system for propositional affine logic (i.e. propositional linear logic with arbitrary weakening). This logic is decidable, but no terminating sequent calculus for it is known. We adapt the history techniques used for intuitionistic and modal logics, but in this case we cannot assume that the context will always be non-decreasing. We show how to overcome this problem, and hence to provide a loop detection mechanism for propositional affine logic.

We consider the problem of searching for proofs in sequential presentations of logics with multiplicative (or intensional) connectives. Specifically, we start with the multiplicative fragment of linear logic and extend, on the one hand, to linear logic with its additives and, on the other, to the additives of the logic of bunched implications ( BI ). We give an algebraic method for calculating the distribution of the side-formulæ in multiplicative rules which allows the occurrence or non-occurrence of a formula on a branch of a proof to be determined once sufficient information is available. Each formula in the conclusion of such a rule is assigned a Boolean expression. As a search proceeds, a set of Boolean constraint equations is generated. We show that a solution to such a set of equations determines a proof corresponding to the given search. We explain a range of strategies, from the lazy to the eager, for solving sets of constraint equations. We indicate how to apply our methods systematically to large family of relevant systems.

Uniform proofs have been presented as a basis for logic programming, and it is known that by restricting the class of formulae it is possible to guarantee that uniform proofs are complete with respect to provability in intuitionistic logic. In this paper we explore the relationship between uniform proofs and classes of formulae more deeply. Firstly we show that uniform proofs arise naturally as a normal form for proofs in first-order intuitionistic sequent calculus. Next we show that the class of formulae known as hereditary Harrop formulae are intimately related to uniform proofs, and that we may extract such formulae from uniform proofs in two different ways. We also give results which may be interpreted as showing that hereditary Harrop formulae are the largest class of formulae for which uniform proofs are guaranteed to be complete. Finally we briefly discuss some possibilites for a slightly more general approach using intermediate and infinitary logics.

In this paper we consider the problem of identifying logic programming languages for linear logic. Our analysis builds on a notion of goal-directed provability, characterized by the so-called uniform proofs, previously introduced for minimal and intuitionistic logic. A class of uniform proofs in linear logic is identified by an analysis of the permutability of inferences in the linear sequent calculus. We show that this class of proofs is complete (for logical consequence) for a certain (quite large) fragment of linear logic, which thus forms a logic programming language. We obtain a notion of resolution proof, in which only one left rule, of clause-directed resolution, is required. We also consider a translation, resembling those of Girard, of the hereditary Harrop fragment of intuitionistic logic into our framework. We show that goal-directed provability is preserved under this translation.