The promotion of well-being across the lifespan, and particularly in later life, has motivated the development of personalized systems that support physical activity, highlighting the need for effective user modeling to foster active ageing. However, if the design of these systems does not explicitly involve older adults, their user models may fail to fully reflect experiential, affective and contextual aspects that are critical for acceptance and sustained engagement. This paper presents EMERGE, a multi-stage participatory elicitation methodology that combines exploration of lived experience and co-design through enacted use scenarios involving older adults, emphasizing an inclusive and intergenerational perspective. A virtual reality system illustrating Tai Chi movements was used throughout the elicitation process, leveraging its immersive nature to support iterative requirements refinement and facilitate changes in participants’ perceptions through direct engagement. Beyond the specific user model dimensions elicited, this work provides methodological insights into participatory elicitation strategies that support the integration of embodied and experiential knowledge from older adults in building adaptive systems for active ageing.

The object-oriented software development process is increasingly used for the construction of complex distributed systems. In this context, behavior models have long been recognized as the basis for systematic approaches to requirements capture, specification, design, simulation, code generation, testing, and verification. Two complementary approaches for modeling behavior have proven useful in practice: interaction-based modeling (e.g., UML sequence diagrams) and state-based modeling (e.g., UML statecharts). Building on formal V&V techniques, in this article we present a method and a tool for automated synthesis of test cases from scenarios and a state-based design model of the application, remaining entirely within the UML framework. The underlying "on the fly" test synthesis algorithms are based on the input/output labeled transition system formalism, which is particularly appropriate for modeling applications involving asynchronous communication. The method is eminently compatible with classical OO development processes since it can be used to synthesize test cases from the scenarios used in early development stages to model global interactions between actors and components, instead of these test cases being derived manually. We illustrate the system test synthesis process using an air traffic control software example

This article describes the technique,symbolicapproximation, that we have evolved to handle the post-hoc verification of C code in very large open source projects such as the Linux kernel, essentially consisting of deliberate approximation in a symbolic domain. Using the technique, we are treating millions of lines of C code source in a few hours on very modest support platforms. The theoretical foundation is a configurable compositional programming logic and a notion of approximation that is tied to what can be deduced about a program, in that adjusting the logic for reasoning about it adjusts the goodness of the approximation to it.

The formal analysis described here detects two so far undetected real deadlock situations per thousand C source files or million lines of code in the open source Linux operating system kernel, and three undetected accesses to freed memory, at a few seconds per file. That is notable because the code has been continuously under scrutiny from thousands of developers' pairs of eyes. In distinction to mo del-checking techniques, which also use symbolic logic, the analysis uses a "3-phase" compositional Hoare-style programming logic combined with abstract interpretation. The result is a customisable post-hoc semantic analysis of C code that is capable of several different analyses at once

Software product families (PF) are becoming one of the key challenges of software engineering. Despite recent interest in this area, the extent to which the close relationship between PF and requirements engineering is exploited to guide the V&V tasks is still limited. In particular, PF processes generally lack support for generating test cases from requirements. In this paper, we propose a requirements-based approach to functional testing of product lines, based on a formal test generation tool. Here, we outline how product-specific test cases can be automatically generated from PF functional requirements expressed in UML (Unified Modeling Language). We study the efficiency of the generated test cases on a case study.

In this article, we investigate the use of the OO computational paradigm for the formulation of knowledge model patterns as OO analysis patterns. We seek to take advantage of research on design pattern specification, aimed at modelling patterns by means of structural and behavioural "meta-level" constraints, introducing appropriate modifications into the UML. We illustrate our argument with the formulation of an OO "assessment pattern" in analogy to the well known "assessment task template".

We report on work concerning the use of object‐oriented analysis and design (OAD) methods in the development of artificial intelligence (AI) software applications, in which we compare such techniques to software development methods more commonly used in AI, in particular CommonKADS. As a contribution to clarifying the role of OAD methods in AI, in this paper we compare the analysis models of the object‐oriented methods and the CommonKADS high‐level expertise model. In particular, we study the correspondences between generic tasks, methods and ontologies in methodologies such as CommonKADS and analysis patterns in object‐oriented analysis. Our aim in carrying out this study is to explore to what extent, in areas of AI where the object‐oriented paradigm may be the most adequate way of conceiving applications, an analysis level ‘pattern language’ could play the role of the libraries of generic knowledge models in the more commonly used AI software development methods. As a case study we use the decision task — its importance arising from its status as the basic task of the intelligent agent — and the associated heuristic multi‐attribute decision method, for which we derive a corresponding decision pattern described in the unified modelling language, a de facto standard in OAD.