Human activity recognition plays an important role especially in medical applications. This paper proposes a formal approach to model such activities, taking into account possible variations in human behavior. This approach is based on discrete-time Markov chains enriched with event occurrence probabilities. We use the PRISM and Storm frameworks and their model checking facilities to express and check interesting temporal logic properties concerning the dynamic evolution of activities. We illustrate our approach on two serious games used by clinicians to monitor Alzheimer patients. This paper focuses on the suitability of such a formal approach to model patients’ behavior, to check behavioral properties of medical interest, and on the respective advantages of the PRISM and Storm frameworks. Our goal is to provide a new tool for doctors to evaluate patients.

The presence of neurocognitive disorders (NCD) must be detected at an early stage of the disease progression and monitored by clinicians overtime, in order to provide early individualized interventions. Today, a reliable diagnosis requires a heavy set of neuropsychological tests, often coupled with biomarker evidence. There is growing interest in finding objective, fast to administer, and reliable behavioral markers that could complement classical clinical assessment and help detecting early changes in cognitive performance. Serious games have been proposed as promising tools to screen cognitive deficits in people with NCD [1]. In this study, we investigated the interest of employing a battery of mini-games developed by CoBTeK lab to distinguish elderly patients with mild NCD from patients without cognitive decline. In the context of an ongoing project, we recruited 20 subjects with mild NCD (14 females; age: M=75.5, SD=5.7; MMSE, M=26.1; SD=2.2) and 10 subjects with subjective cognitive decline - SCD (9 females; age: M=71.0, SD=7.6; MMSE, M=29.2, SD=1.2) at the Nice Memory Center. Participants played four mini-games on a tablet, each game assessing a different cognitive function: selective and sustained attention, episodic memory, inhibitory control, and sensitivity to reward. We collected different data including scores, responses, response times, and videos (focused on hand gestures). Preliminary data analysis focused on one mini-game (assessing sensitivity to reward) suggests that participants with mild NCD had an almost significantly lower sensitivity to reward. Once the data analysis is complete for the 4 mini-games, and the final sample size of 50 participants is reached (by the end of June 2021), we plan to integrate all the collected data into a predictive behavior model compliant with model checking techniques. Converging with previous findings, these very preliminary results suggest that mini-games could be interesting to differentiate patients with mild NCD from subjects without cognitive impairment. Predictive behavior model based on mini-games may in the next future help clinicians identify individuals that meet the profile of NCD. Reference: Robert P et al. (2014) Recommendations for the use of Serious Games in people with Alzheimer’s Disease, related disorders and frailty. Front Aging Neurosci . 6:54. doi:10.3389/fnagi.2014.00054

Human activity recognition plays an important role especially in medical applications. This paper proposes a formal approach to model such activities, taking into account possible variations in human behavior. Starting from an activity description enriched with event occurrence probabilities, we translate it into a corresponding formal model based on discrete-time Markov chains (DTMCs). We use the PRISM framework and its model checking facilities to express and check interesting temporal logic properties (PCTL) concerning the dynamic evolution of activities. We illustrate our approach on the model of a serious game used by clinicians to monitor Alzheimer patients. We expect that such a modeling approach could provide new indications for interpreting patient performances. This paper addresses only the model definition and its suitability to check behavioral properties of interest. Indeed, this is mandatory before envisioning any clinical study.

Activity Recognition aims at recognizing and understanding sequences of actions and movements of mobile objects (human beings, animals or artefacts), that follow the predefined model of an activity. We propose to describe activities as a series of actions, triggered and driven by environmental events. Due to the large range of application domains (surveillance, safety, health care ...), we propose a generic approach to design activity recognition systems that interact continously with their environment and react to its stimuli at run-time. In our target applications, the data coming from sensors (video-cameras, etc.) are first processed to recognize and track objects and to detect low-level events. This low-level information is collected and transformed into higher level inputs to our activity recognition system. Such recognition systems must satisfy stringent requirements: dependability, real time, cost effectiveness, security and safety, correctness, completeness ... To enforce most of these properties our approach is to base the configuration of the system as well as its execution on formal techniques. We chose the synchronous approach which provides formal bases to perform static analysis, verification and validation, but also direct implementation. Several synchronous languages such as Lustre, Esterel, Scade and Signal [2] have been defined to describe synchronous automata. These languages are for expert users. We propose a new user-oriented language, named ADeL (Activity Description Language) to express activities and to automatically generate recognition automata. This language is easier to understand and to use by non computer scientists (e.g., physicians) while relying on formal semantics.

Activity Recognition aims at recognizing and understanding sequences of actions and movements of mobile objects (human beings, animals or artefacts), that follow the predefined model of an activity. We propose to describe activities as a series of actions, triggered and driven by environmental events. Due to the large range of application domains (surveillance, safety, health care ...), we propose a generic approach to design activity recognition systems that interact continously with their environment and react to its stimuli at run-time. In our target applications, the data coming from sensors (video-cameras, etc.) are first processed to recognize and track objects and to detect low-level events. This low-level information is collected and transformed into higher level inputs to our activity recognition system. Such recognition systems must satisfy stringent requirements: dependability, real time, cost effectiveness, security and safety, correctness, completeness ... To enforce most of these properties our approach is to base the configuration of the system as well as its execution on formal techniques. We chose the synchronous approach which provides formal bases to perform static analysis, verification and validation, but also direct implementation. Several synchronous languages such as Lustre, Esterel, Scade and Signal [2] have been defined to describe synchronous automata. These languages are for expert users. We propose a new user-oriented language, named ADeL (Activity Description Language) to express activities and to automatically generate recognition automata. This language is easier to understand and to use by non computer scientists (e.g., physicians) while relying on formal semantics.

Many important and critical applications such as surveillance or healthcare require some form of (human) activity recognition. Activities are usually represented by a series of actions driven and triggered by events. Recognition systems have to be real time, reactive, correct, complete, and dependable. These stringent requirements justify the use of formal methods to describe, analyze, verify, and generate effective recognition systems. Due to the large number of possible application domains, the researchers aim at building a generic recognition system. They choose the synchronous approach because it has a well-founded semantics and it ensures determinism and safe parallel composition. They propose a new language to represent activities as synchronous automata and they supply it with two complementary formal semantics. First a behavioral semantics gives a reference definition of program behavior using rewriting rules. Second, an equational semantics describes the behavior in a constructive way and can be directly implemented. This paper focuses on the description of these two semantics and their relation.

Activity recognition is important for security and safety in many domains, such as surveillance and health care. We propose to describe activities as a series of actions, triggered and driven by environmental events. We rely on synchronous automata to describe such activities. We chose the synchronous paradigm because it has a well-founded semantics and it ensures determinism and parallel composition. Moreover, we already developed tools that can be adapted to activity recognition. In this report we propose a new synchronous language to express synchronous automata, that relies on a formal semantics and that al- lows us to perform model-checking proofs, to compile activities into equation systems, and to automatically generate the corresponding recognition code.

Activity recognition aims at recognizing and understanding the movements, actions, and objectives of mobile objects. These objects can be humans, animals, or simple artefacts. Many important and critical applications such as surveillance or health care require some form of (human) activity recognition. Existing languages can be used to describe models of activities, but they are difficult to master by non computer scientists (ex: doctors). In this paper, we present a new language dedicated to end users, to describe their activities. We call it ADeL (Activity Description Language). This language is intended to be part of a complete recognition system. Such a system has to be real time, reactive, correct, and dependable. We choose the synchronous approach because it respects these characteristics, it ensures determinism and safe parallel composition, and it allows verification of systems using model-checking. Relying on the synchronous approach, we supply our language with two complementary formal semantics and we provide it with two formats: textual and graphical. This paper focuses on the description of the ADeL language.

One of the biggest challenges in hardware and software design is to ensure that a system is error-free. Small defects in reactive embedded systems can have disastrous and costly consequences for a project. Preventing such errors by identifying the most probable cases of erratic system behavior is quite challenging. Indeed, tests performed in industry are non-exhaustive, while state space analysis using formal verification in scientific research is inappropriate for large complex systems. We present in this context a new approach for generating exhaustive test sets that combines the underlying principles of the industrial testing technique with the academic-based formal verification. Our method consists in building a generic model of the system under test according to the synchronous approach. The goal is to identify the optimal preconditions for restricting the state space of the model such that test generation can take place on significant subspaces only. So, all the possible test sets are generated from the extracted subspace preconditions. Our approach exhibits a simpler and efficient quasi-flattening algorithm compared with existing techniques, and a useful compiled internal description to check security properties while minimizing the state space combinatorial explosion problem. It also provides a symbolic processing technique for numeric data that provides an expressive and concrete test of the system, while improving system verification (Determinism, Death sequences) and identifying all possible test cases. We have implemented our approach on a tool called AUTSEG V2. This testing tool is an extension of the first version AUTSEG V1 to integrate data manipulations. We present in this paper a complete description of our automatic testing approach including all features presented in AUTSEG V1 and AUTSEG V2.

This paper deals with dynamic adaption of software architecture in response to context changes. In the line of “models at run time”, we keep a model of the system and its context in parallel with the running system itself. We adopted an enriched Feature Model approach to express the variability of the architecture as well as of the context. A context change is transformed into a set of feature modifications (selection/deselection) that we validate against the feature model to yield a new suitable and valid architecture configuration. Then we update the model view of the configuration and the running system architecture accordingly. The paper focuses on the feature model reconfiguration step and details the algorithms and heuristics that implement our adaptation rules. The approach is illustrated with a simple example borrowed from the videosurveillance domain. The efficiency of the algorithm is evaluated on randomly generated feature models (from 60 to 1400 features). Our results show that in our target applications (video analysis), the processing time of a context change may be considered negligible.

Feature modeling has been widely used in domain engineering for the development and configuration of software product lines. A feature model represents the set of possible products or configurations to apply in a given context. Recently, this formalism has been applied to the runtime (re-)configuration of systems with high variability and running in changing contexts. These systems must adapt by updating their component assembly configuration at runtime, while minimizing the impact of such changes on the quality of service. For this reason the selection of a good system configuration is seen as an optimization problem based on quality attribute criteria.

Feature modeling has been widely used in domain engineering for the development and configuration of software products. A feature model represents the set of possible configurations to apply in a given context. Recently, this formalism was applied to the runtime (re-)configuration of systems with high variability and context changes, in which the selection of the best candidate configuration is seen as an optimization problem based on quality criteria. To this end, we propose an approach for the specification, measurement and optimization of runtime quality attributes based on feature models, and furthermore, we describe its integration into a component-based architecture for supporting dynamically adaptive systems. Feature models are annotated with quality-attribute properties and metrics, and then an efficient and flexible algorithm is used to deal with the optimization problem. We report on some examples of adaptation and quality-attribute scenarios in the context of a video surveillance domain, in order to illustrate the pros and cons of our approach.

Feature models are widely used to capture variability, commonalities and configuration rules of software systems. We apply this technique to model component-based systems with many variants during specification, implementation, or run time. This representation allows us to determine the set of valid configurations befitting a given context, especially at run time. A key challenge is to determine the configuration most suitable, especially with respect to non-functional aspects: quality of service, performance, reconfiguration time... We propose an algorithm for selecting the configuration that optimizes a given quality metrics. This algorithm is a variant of the Best-First Search algorithm, a heuristic technique suitable for feature model optimization. The algorithm is parameterized with several strategies and heuristics on feature models leading to different optimality and efficiency properties. We discuss the algorithm, its strategies and heuristics, and we present experimental results showing that the algorithm meets the requirements for our real time systems.

Building large scale systems involves many design decisions, both at specification and implementation levels. This is due to numerous variants in the description of the task to achieve and its execution context as well as in the assembly of software components. We have modeled variability for large scale systems using feature diagrams, a formalism well suited for modeling variablility. These models are built with a clear separation of concerns between specification and implementation aspects. They are used at design and deployment time as well as at execution time. Our test application domain is video surveillance systems, from a software engineering perspective. These are good candidates to put model driven engineering to the test, because of the huge variability in both the surveillance tasks and the video analysis algorithms. They are also dynamically adaptive systems, thus suitable for models at run time approaches. We propose techniques and tools to define the models, to operate on them, and to transform specification requirements into an effective implementation of a processing chain. We also define a run time architecture to integrate models into the adaptation loop.

Modern vision systems must run in continually changing contexts. For example, a system to detect vandalism in train stations must function during the day and at night. The vision components for acquisition and detection used during daytime may not be the same as those used at night. The system must adapt to a context by replacing running components such as image acquisition from color to infra-red. This adaptation must be dynamic with detection of context, decision on change in system configuration, followed by the seamless execution of the new configuration. All this must occur while minimizing the impact of dynamic change on validity of detection and loss in performance. We present Girgit, a context-aware vision system for scene understanding, that dynamically orchestrates a set of components. A component encapsulates a vision-related algorithm such as from the OpenCV library. Girgit inherently provides loading/caching of multiple component instances, system reconfiguration, management of incoming events to suggest actions such as component re-configuration and replacement of components in pipelines. Given the surplus architectural layer for dynamic adaptation one may ask, does Girgit degrade scene understanding performance? We perform several empirical evaluations on Girgit using metrics such as frame-rate and adaptation time to answer this question. For instance, the average adaptation time between change in configurations is less than 2 μs with caching, while 8 ms without caching. This in-turn has negligible effect on scene understanding performance with respect to static C++ implementations for most practical purposes.