Lydia Jaß
email: lydia.jass@tu-berlin.de

Paula Herber
email: paula.herber@tu-berlin.de

Bit-Precise Formal Verification for SystemC using Satisfiability Modulo Theories Solving

Hardware/software codesigns are often modeled with the system level design language SystemC. Especially for safety critical applications, it is crucial to guarantee that such a design meets its requirement. In this paper, we present an approach to formally verify SystemC designs using the UCLID satisfiability modulo theories (SMT) solver. UCLID supports finite precision bitvector arithmetics. Thus, we can handle SystemC designs on a bit-precise level, which enables us to formally verify deeply integrated hardware/software systems that comprise detailed hardware models. At the same time, we exploit UCLID's ability to handle symbolic variables and use k-inductive invariant checking for SystemC designs. With this inductive approach, we can counteract the state space explosion problem, which model checking approaches suffer from. We demonstrate the practical applicability of our approach with a SystemC design that comprises a bit-and cycle-accurate model of a UART and software that reads data from the UART.

Introduction

Embedded systems are ubiquitous in today's everyday life, and they are often used in safety-critical applications, e.g. in airplanes or cars. A failure of such a system can lead to high financial losses and even human injuries or deaths. This makes it crucial to verify their correctness under all circumstances.

One of the main challenges for embedded systems verification is that the systems usually consist of deeply integrated hardware and software components. There already exists a large variety of validation and verification techniques for integrated HW/SW systems. However, the validation techniques are mostly non-systematic and incomplete, such as simulation and testing. These techniques cover neither the whole design nor all possible input scenarios. Opposed to that, formal methods have the advantage of covering all possible input scenarios and all possible behaviors of a given system. However, most of the existing formal verification techniques for hardware/software codesigns are either tailored to hardware or to software verification and can not cope well with designs that contain both bit-precise hardware models and high-level software.

In this paper, we present an approach to overcome this problem by using the UCLID verification system. The UCLID system is used to specify and verify systems modeled at the term level, and thus provides adequate abstractions for the representation of high-level software. At the same time, it supports the theories of bitvector arithmetics and of arrays. As underlying verification technique, UCLID uses a powerful Satisfiability Modulo Theory (SMT) solver supporting both eager and lazy SMT solving and the constructed formulas can be checked with any state-of-the-art SAT solver. Together, this makes UCLID a powerful tool for (bit-precise) system level design verification.

Our main contribution is a fully-automatic transformation of digital HW/SW co-designs that are modeled in SystemC into the UCLID specification language. The transformation enables us to apply the UCLID SMT solver to SystemC designs and thus to prove important properties like reliable safety and timing behavior. UCLID has the potential to cover most of the expressiveness of SystemC, including discrete time, static and dyanamic sensitivity, inter-process communication and bit-vector arithmetics. Our representation of SystemC designs in UCLID and UCLID's symbolic simulation mechanism enable scalable verification using k-inductive invariant checking. By using inductive verification, we avoid the state space explosion problem that model checking approaches typically suffer from. We demonstrate the scalability and practical applicability of our approach with two case studies. The first is a simple producer-consumer example, where we use varying buffer sizes. The second case study is a typical industrial HW/SW codesign, namely a bit-and cycle-accurate model of a UART together with a software component that reads data from the UART.

The paper is structured as follows: In Sec. 2, we briefly introduce SystemC, UCLID, and k-inductive verification. In Sec. 3, we discuss related work. We present our transformation from SystemC to UCLID in Sec. 4. We discuss experimental results in Sec. 5 and conclude in Sec. 6.

Preliminaries

SystemC

SystemC is a system-level design language and a framework for HW/SW cosimulation. The semantics of SystemC is informally defined in an IEEE standard [START_REF]IEEE Standards Association: IEEE Std. 1666-2011, Open SystemC Language Reference Manual[END_REF]. It is implemented as a C++ class library, which provides language elements for the description of hardware and software, and allows for modeling of both hardware and software components on various levels of abstraction. It also features an event-driven simulation kernel, which enables the simulation of the design. A SystemC design consists of a set of communicating processes, triggered by events and interacting through channels. Modules and channels represent structural information. SystemC also introduces an integer-valued time model with arbitrary time resolution. Listing 1.1 shows an excerpt of a SystemC producer module that writes to a FIFO buffer. The produce method (which is executed within an SC THREAD process) contains an infinite loop where the producer writes a value between 0 and 32 to the fifo port at every clock cycle.

The execution of SystemC designs is controlled by the SystemC scheduler. Like typical hardware description languages, SystemC supports the notion of delta-cycles, which impose a partial order on parallel processes. Note that the order in which processes are executed within a delta-cycle is not specified in [START_REF]IEEE Standards Association: IEEE Std. 1666-2011, Open SystemC Language Reference Manual[END_REF], i. e., it is inherently non-deterministic.

UCLID

UCLID is a verification system developed in a joint project by Carnegie Mellon University and University of California, Berkeley [START_REF] Lahiri | The UCLID Decision Procedure[END_REF]. It incorporates a decision procedure to verify (possibly infinite) state systems. The specification language supports uninterpreted functions, bit-vector arithmetic and lambda expressions. UCLID can handle symbolic simulation, which allows a design to be verified for an arbitrary start state and thus enables an inductive verification approach.

A UCLID module consists of inputs, variables, constants, macros, and assign expressions. The assign expressions define the state variables and the transition relation of the underlying labeled transition system. UCLID interprets the model together with the property to be verified as one formula and supports eager and lazy Satisfiability Modulo Theories (SMT) solving.

K-Inductive Invariant Verification

For k-inductive invariant checking [START_REF] Sheeran | Checking safety properties using induction and a SAT-solver[END_REF], two models are needed. One explicit model representing the system from its initial state, and one symbolic model that represents the system in an arbitrary state. Desired properties are expressed as a predicate P(x), which determines whether a requirement P holds in simulation step x of a given model. k-inductive invariant checking is done in two steps:

1. Base case: Simulate the explicit model k steps from its initial state and check P (0) ∧ ... ∧ P (k). 2. Induction: Symbolically simulate the symbolic model from an arbitrary initial state for k+1 steps. Then check P (0) ∧ ... ∧ P (k) =⇒ P (k + 1).

If there exists a k so that both base cases can be shown, then the property under verification holds in all reachable system states. If the property under verification does not hold, the system is unsafe and we get a counter example. Note that the counter example may be spurious if k is too small.

There exist several approaches to the automated formal verification of SystemC designs. For example, in [START_REF] Habibi | Generating Finite State Machines from Sys-temC[END_REF], the authors propose program transformations from SystemC into state machines, but they ignore time, the transformation is performed manually, and hardware data types are not explicitly considered. Karlsson et al. [START_REF] Karlsson | Formal verification of SystemC Designs using a Petri-Net based Representation[END_REF] verify SystemC designs using a petri-net based representation and the PRES+ model checker. However, the petri-net based approach introduces a huge overhead because interactions can only be modeled by introducing additional subnets. As it is based on model checking, the approach also suffers from the state space explosion problem. Bit-precise hardware data types are not explicitly considered. In [START_REF] Herber | Model Checking SystemC Designs Using Timed Automata[END_REF][START_REF] Pockrandt | Model checking memory-related properties of hardware/software co-designs[END_REF], an approach for the formal verification of SystemC designs using the model checker UPPAAL is presented. A large subset of SystemC is supported. However, UPPAAL does not support inductive verification techniques and thus suffers from the state space explosion problem. Furthermore, it is not well-suited to support hardware data types. In [START_REF] Große | Proving Transaction and System-level Properties of Untimed SystemC TLM Designs[END_REF], bounded model checking is used on untimed SystemC TLM designs. They use k-inductive invariant checking using CBMC [START_REF] Clarke | A tool for checking ANSI-C programs[END_REF] and Boolector [START_REF] Brummayer | Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays[END_REF] as underlying SMT solver. This work is very close to our approach. The main idea is to transform a given SystemC TLM design into a sequential C program and perform loop unwinding to achieve a complete model. However, compared to our approach, they only support a small subset of untimed SystemC TLM designs and disregard time and complex process interactions. Furthermore, bit-precise hardware data types are not explicitly considered.

In [START_REF] Garavel | Verification of an industrial SystemC/TLM model using LOTOS and CADP[END_REF][START_REF] Helmstetter | TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox[END_REF], an encoding from SystemC into the verification toolbox CADP is proposed. This approach is based on a manual definition of callback functions, which are then used to natively execute SystemC/C++ code in the CADP verification system. Still, the transformation has to be done manually. Furthermore, bit-precise hardware data types are not explicitly considered. In [START_REF] Cimatti | Software model checking systemc[END_REF], Cimatti et al. generate three different verification models from a given SystemC design, each tailored to a specific aspect of the SystemC semantics on different levels of abstraction, and use software model checking techniques. While this approach is capable of handling the most important SystemC constructs including time and communication, it can not handle bit-precise hardware data types. Furthermore, by using model checking techniques, it also suffers from the state space explosion problem. In [START_REF] Elshuber | Improving systemlevel verification of systemc models with spin[END_REF], the authors present an approach for the verification of SystemC designs using the software model checker SPIN. Again, by using a software model checker, they suffer from the state space explosion problem.

Note that there also exist some approaches to automated formal verification of other system level design languages. For example, in [START_REF] Chang | Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories[END_REF], the authors present an approach for formal deadlock analysis of SpecC models using SMT. However, they only consider the timing relations in a given design by formulating assertions over time stamps, which are assigned to executable code. This is sufficient for a deadlock analysis but does not allow for checking of other functional or nonfunctional properties.

The key idea of our approach for the bit-precise verification of SystemC designs using satisfiability modulo theories solving is to transform a given SystemC design into a semantically equivalent UCLID specification. Our transformation preserves the (informally defined) bit-precise semantics of a given SystemC designs. The main challenges are to preserve the sequential simulation semantics of SystemC in a synchronous target language, i. e., to model the non-deterministic execution semantics of the SystemC scheduler, and to respect the bit-precise semantics of all data operations. The basic idea of our transformation is to translate all SystemC processes into UCLID state machines, and to control the execution of these processes by modeling the SystemC scheduler and SystemC events as UCLID state machines. To capture the simulation semantics of Sys-temC, our UCLID model of the scheduler interprets the operational sequences of the SystemC kernel, which manages process scheduling and channel updates.

The transformation result is a UCLID interpretation of the semantics of the given SystemC design. This can then be automatically verified using the UCLID verification system. The main advantage of our approach is that the formal semantics we define for SystemC by translating it into the formal specification language of UCLID is bit-precise, and that the underlying verification engine is based on SMT solving and thus enables inductive proofs.

Assumptions

The following assumptions on a SystemC design define our supported subset. If all of these assumptions are fulfilled, we can transform a given SystemC design automatically into a semantics-preserving UCLID representation and verify it using the UCLID verification system.

Representation of SystemC Designs in UCLID

Our representation of a SystemC design in UCLID interprets the simulation semantics of SystemC. This means that not only all the SystemC modules of the design are represented in UCLID, but also the scheduler, processes, events and primitve channels, which altogether define the execution semantics. SystemC modules contain processes, events and member variables. Module ports are connected to channels, which provide communication methods between modules. Before simulation, the SystemC kernel creates the module hierarchy in its elaboration phase and performs instantiation and binding. In this phase, all module, channel, and process objects are created and bound together. Because UCLID does not support dynamic module creation, we recreate the SystemC design after elaboration. This means we create UCLID modules for all module and channel instances and their connections. As a preprocessing step for our transformation from SystemC to UCLID, we flatten the design. The hierarchical structure is kept transparent in the UCLID specification using prefixes. To capture the state of a given SystemC design, we use the following state variables:

(1) All local and global variables, including all module and all channel variables, (2) the state of each process (including its current program counter), (3) the state of each event, (4) the state of the SystemC scheduler. The structure of our representation of SystemC designs in UCLID is shown in Fig. 1. To capture the static part of a design, we create modules for each channel and module (or, more general, struct) instance. The communication methods provided by a channel are placed within the corresponding UCLID module that represents the channel instance. To capture the simulation semantics, we create modules for the scheduler and the simulation time, and for all processes and events of a given design. We distinguish between an internal process module, which keeps track of the program counter and performs event notifications and channel accesses, and a process module, which determines the state of the process, and reacts to events to implement static and dynamic sensitivity.

Scheduler and Simulation Time

We have defined two separate UCLID modules for the scheduler and simulation time. The scheduler module nondeterministically chooses the next runnable process and defines the phase the system is in (initialize, evaluate, update, or advance time). The simulation time module manages the advancement of time. In the advance time phase, the simulation time module advances time to the earliest pending timed notification.

Processes Processes are SystemC's units of execution. For each process, we introduce two modules. The internal process module ipm keeps track of the program counter, notifies events and accesses channels. The process module pm determines the state the process is in, and reacts to events to implement static and dynamic sensitivity. When the scheduler chooses a process to be running, its process module changes its state to running. This triggers the internal process module, which runs until it reaches a wait statement or the process terminates. An excerpt of the internal process module ipm is shown in Listing 1.2. It realizes a state machine that keeps track of the program counter and evaluates control flow conditions. The internal state istate is first set to initialized. As soon as the state of the process module pm is set to running, istate is set to the first program counter label line9 while loop where a while loop is entered. Then, istate is set to the label line11 call wait. Next, the process is suspended and waits to become runnable again. Function calls are realized by a similar mechanism. For example, the write method of the channel module fifo is started if the internal state is set to line13 call write. It returns control to the produce process by setting its program counter to fifo done. Note that we did not include a program counter label for each line of code in the istate state machine. Instead, we reduced the set of program counter labels to represent the necessary atomic blocks. An atomic block comprises a sequence of states in the control flow without branches or process suspension. As SystemC uses a cooperative scheduler, atomic blocks can never be interrupted. Thus, it is possible to abstract from some intermediate steps and to combine multiple sequential actions in one (synchronous) simulation step as long as we ensure that no data race may occur. So far, we just exclude cases where a potential data race may occur from this optimization. The benefit of the reduction is a smaller UCLID model while preserving the execution semantics of SystemC.

An excerpt of the process module pm is shown in Listing 1.3. It implements the process state, which may be one of process initialized, running, runnable, process done, wait t, wait e, or wait s (the latter to wait for a given time, an event or for the sensitivity list, respectively). Note that pm makes use of the current state of ipm, the current process selected by the scheduler, and the current state of the FIFO channel. The latter is necessary because the process might be suspended by a wait call that occurs within the FIFO channel. Events We create one UCLID module for each event. Additionally, we also create timeout event modules for processes that suspend themselves by calling a timed wait. Processes may notify events immediately, delta-delayed or timed. If a process performs an immediate notification of an event, the event immediately occurs and all processes that are sensitive to the event react by changing their states. For a delta-delayed notification, the notification is delayed until the next delta-cycle starts. If a process performs a timed notification, the event adopts the time value and waits until the simulation time is equal to the target time. If a process calls the wait function without any argument, its process module waits for one of the events from the processes sensitivity list to occur. New notifications overwrite pending notifications if they expire at an earlier target time.

An excerpt of a UCLID event module is shown in Listing 1.4. Initially, the event state estate is set to no notification. Then, it reacts to all processes that might notify the event and sets the state to immediate, delta or timed accordingly. The event state is reset if occurred becomes true. This happens whenever an immediate notification occurs, if we have a pending delta-delayed notification and the scheduler starts a new delta cycle, or if we have a pending timed notification and the simulation time becomes equal to the target time. Channels For each channel, we create a module that contains all channel variables and all communication methods for all process modules that might call those methods. If a channel method waits for an event to occur, the caller process module changes its state to also wait for the event. Primitive channels implement the request-update semantics. This means that they do not change the state of the channel directly. Instead, they request the channel to be updated during the update phase. For this purpose, primitive channels have a dedicated update method, which is executed in the update phase after all evaluations are finished. In UCLID, we represent this mechanism by setting a request update variable in the channel module that activates an update state machine.

Variables Beside process and event states, the state of a SystemC design comprises local and global variables. Using the program counter labels described above, we can decide for each variable at what points in the program it is manipulated. Using this information, we can construct one UCLID state machine for each variable of a given SystemC design. An example for a state machine that models the local variable c of our running example is shown in Listing 1.5.

Note that in UCLID, a declaration of a variable does not ensure that the given number of bits is used for its representation. Instead, UCLID always uses as few bits as possible. To ensure that the bit-precise semantics of SystemC is preserved, we use the correct bitwidth for all arithmetic and logic operations and we cast all expressions into the left hand side types within assignments.

So far, we support boolean-and int-typed variables, sc int and sc uint, arrays, and structs. We represent boolean types by UCLID's TRUTH type. The types int, sc int and sc uint are represented as bitvectors using UCLID's BITVECtype with the specified length respectively. Arrays are modeled using lambdaexpressions, as described in the UCLID documentation [START_REF] Brady | A User's Guide to UCLID[END_REF].

Verification of SystemC Designs using UCLID

With our representation of SystemC designs within UCLID as described above, we can automatically transform a given SystemC design into a UCLID specification. Then, it can symbolically be simulated and verified in UCLID using k-inductive invariant checking [START_REF] Sheeran | Checking safety properties using induction and a SAT-solver[END_REF]. To adapt k-inductive invariant checking with UCLID, we create an explicit UCLID model and check the base case and a symbolic model for the induction, as described in Sec. 2.3. The explicit model starts in the same state as the SystemC design. For the symbolic model, we set all state variables to symbolic constants (for truth types, bitvectors and bitvector functions) or non-deterministic choice variables (for enum variables) respectively. If UCLID returns a counter example, it might be spurious, i.e. it might not be reachable by the original system. If UCLID returns that the induction step is valid, we can conclude that the system never violates the requirement and it is safe. There is no straightforward way to determine the value of k needed to prove or disprove a property. Thus, we incrementally increase k until we reach a predefined maximum value of k or the counter example is not spurious.

Evaluation

We have implemented our transformation from SystemC to UCLID in Java. The resulting framework is shown in Fig. 2. A given SystemC design is preprocessed and translated into our SystemC intermediate representation SysCIR. There, we flatten the design and resolve all port and channel connections. Our novel transformation engine then generates an explicit and a symbolic UCLID model. Those are then used for k-inductive invariant checking as described above.

To evaluate our approach, we use two case studies and compare the verification times with those achieved with UPPAAL [START_REF] Herber | Model Checking SystemC Designs Using Timed Automata[END_REF][START_REF] Pockrandt | Model checking memory-related properties of hardware/software co-designs[END_REF]. In the first case study, two producers and one consumer communicate over a FIFO buffer (3 processes, 1 channel). The second case study is a more complex UART design that consists of a bit-and cycle-accurate UART model and software that reads data from the UART (7 processes, 9 channels). We ensure that we cover all possible input scenarios by modeling input data using selections in UPPAAL and symbolic constants in UCLID. Note that the UART case study could not be handled with the approach presented in [START_REF] Große | Proving Transaction and System-level Properties of Untimed SystemC TLM Designs[END_REF]. All experiments were performed on a 64 bit Linux system with an Intel Core i7-4770 with 3.2 GHz and 32 GB main memory. All designs are transformed into UCLID respectively UPPAAL in less than a second. We have shown that the producer-consumer example does not cause a buffer over-or underflow with our k-inductive invariant checking approach. The requirement we check is P (i) := fifo.n ≤ BS ∧ fifo.n ≥ 0. To verify this, k must at least be 10. This corresponds to the maximum number of steps until the desired property is restored from an arbitrary start state. To evaluate the scalability of our approach, we have varied the buffer size from 10 to 1000. As Table 1 shows, the time it takes UCLID to verify the model with growing buffer capacities stays nearly constant, while the verification time in UPPAAL increases exponentially.

For the UART system, we verify that the software correctly reads all data that is sent over the UART. The requirement we check is P (i) := sw.error cnt ≤ 0, where error cnt is used in the software component sw to mark if the values differ. To verify the UART system, k must at least be 200. We evaluated the scalability by varying the bitwidth of the transmitted data from 4 bit to 32 bit. Table 1 shows the runtimes of both bounded model checking and the induction step. Although the computational effort is considerable, we achieve a complete proof for all possible input scenarios, and the verification time is similar for varying bitwidths. UPPAAL is able to verify the 4-bit system in less time, but exceeds resources for all larger bitwidths1 .

Conclusion

In this paper, we have presented an automatic transformation from SystemC to the formal verification system UCLID. Our transformation is able to cover a large subset of SystemC including static and dynamic sensitivity, time, primitive channels, and bit-precise hardware data types. To capture the semantics of a given SystemC design, we translate all variables and processes into UCLID state machines, and we provide predefined state machines that model the execution semantics of SystemC and the event notification mechanism. The structure of the original design is kept transparent by using prefixing. This eases comprehensibility of counter examples. With the result of our transformation, we can use UCLID's powerful verification mechanisms and underlying SMT solver to verify a given SystemC design using k-inductive invariant checking.

To demonstrate the practical applicability of our approach, we have used a simple producer-consumer example taken from the SystemC reference implementation and an industrial UART system. We have shown that our approach scales well for increasing data ranges and bit widths, which is typically not the case for model checking based approaches. With the UART system, we have also shown the applicability of our approach to (small) industrial applications.

In future work, we plan to optimize our transformation by allowing parallel executions whenever we can safely assume that no data race may occur. We are confident that in doing so, we can significantly reduce the necessary k for k induction, which in turn will significantly reduce the verification effort.

  DEFINE occurred := case ((estate = immediate) | ((estate = delta) & scheduler.new delta) | ((estate = timed) & (t = sim time.time))) : true; default : false; esac; ASSIGN init[estate] := no notification; next[estate] := case occurred : no notification; ( * reset the event state * ) process.notify event immediate : immediate; ((estate != immediate) & process.notify event delta) : delta; ((estate != immediate) & (estate != delta) & process.notify event timed) : timed; default : estate; esac; init[t] := ... Listing 1.4. Event Module

Fig. 2 .

 2 Fig. 2. Framework for Verifying SystemC Designs with UCLID

1 .

 1 No dynamic variable or process creation. 2. No recursion. 3. No inheritance nor pointers, no side effects. 4. No external code or library calls. 5. For division and modulo operations the divisor is an integer power of 2. 6. So far, we only support boolean and integer variables with fixed bit width, and arrays and structs thereof.

  Excerpt of the Process Module pm

	DEFINE
	sensitivity list occurred := case clk edge event.occurred : true;
	default : false; esac;
	ASSIGN
	init[state] := process no state;
	next[state] := case
	(ipm.istate = initialized) : process initialized;
	(state = process initialized) : runnable;
	((scheduler.next = produce) & (scheduler.current = none)) : running;
	((state = wait s) & sensitivity list occurred) : runnable;
	(ipm.istate = done) : process done;
	(ipm.istate = line11 call wait) : wait s;
	(ipm.istate = line13 wait for write & fifo.write = line31 call wait) : wait e;
	(ipm.istate = line13 wait for write & r event.occurred & state = wait e) : runnable;
	default : state;
	esac;
	Listing 1.3.

Table 1 .

 1 Verification Times in [hh:]mm:ss

		Producer-Consumer		UART system
	buffer size/bitwidth 10 50 100 1000	4	8	16	24	32
	BMC	< 1 < 1 < 1	< 1 10:30 10:25 10:03 10:07 10:03
	k-induction	0:06 0:06 0:06	0:06 7:22:00 7:03:00 7:11:00 6:40:00 7:11:32
	UCLID Total	0:06 0:06 0:06	0:06 7:32:30 7:13:25 7:21:03 6:50:07 7:21:35
	UPPAAL Total	0:02 0:02 0:09 3:00:51 2:42:40	x	x	x	x

UPPAAL did not return results after 48 hours while using 32 GB main memory.


Maurício Fontana De Vargas

Carlos Eduardo Pereira
email: cpereira@ece.ufrgs.br

Ontological User Modeling for Ambient Assisted Living Service Personalization

Keywords: Ontology, Context-aware, Functioning, User Centered, World Health Organization

Given that the population is aging, it is crucial to develop technologies which will not only help the elderly to age in place, but also live in place with independent and healthy lifestyle. Ambient Assisted Living (AAL) environments can help the elderly and people with functional diversity by anticipating their needs in specific situations and acting proactively in order to properly assist them in performing their activities of daily living (ADLs). Since the users needs tend to be very diverse in regard to functioning and disability levels, it is crucial to have personalized services capable of providing tailored assistance to a user based on their unique preferences, requirements, and desires. This paper introduces the ontology named AATUM (Ambient Assistive Technology User Model), to be adopted by systems whose goal is to enhance user quality of life within ALL environments through service personalization. Its main feature is the use of The International Classification of Functioning, Disability and Health (ICF) to model the user's functioning and disability levels in a consistent and internationally comparable way. The use of the proposed ontology is illustrated through its application in two different case studies.

Introduction

The percentage of global population aged 60 or older is expected to be 22% by 2050 [START_REF] Lutz | The coming acceleration of global population ageing[END_REF]. As a result, there is an expected increase of chronic illnesses and disability associated with old age. This demographic change toward an aging society results in many social and health care system challenges to ensure that our infrastructures can support the needs of the elderly, enabling them to have an independent and healthy lifestyle.

Given the fact that 64% of older adults prefer to stay in the comfort of their own homes, and given the costs of nursing home care, it is crucial to develop technologies that help older adults not only to age, but also live in place i.e, independently and comfortably in their home [START_REF] Disease Control | The state of aging and health in america 2013[END_REF].

In recent years, researchers have developed a variety of assistive technologies based on a the paradigm called "ambient intelligence", where the ambient anticipates users needs in specific situations and acts proactively in order to properly assist the user to perform his/her activities of daily living (ADLs). Assisted living technologies based on ambient intelligence are called Ambient Assisted Living (AAL) tools and can be used for preventing, healing, and improving quality of life of the elderly and people with functional diversity.

Since these users tend to be greatly variable in regards to functioning and disability levels, service personalization is crucial [START_REF] Kadouche | Personalization in smart homes for disabled people[END_REF]. A personalized service is a service capable of providing tailored assistance to a user based on their unique preferences, requirements, and desires. Therefore, service personalization within AAL environments can help elderly people or people with functional diversity to increase their independence and quality of life.

The need for service personalization has led to the use of ontologies as a means to provide a correct user model in a machine understandable format. This model is generally represented in the form of a user profile which captures the personal aspects in terms of user's behaviors, goals, capacities, likes and dislikes. Therefore, the user model can be seen as an abstract entity and the user profile represents an instantiation of the user model for a specific user [START_REF] Bhowmick | Ontology based user modeling for personalized information access[END_REF].

This work focuses on user modeling using an ontology to enhance user quality of life within ALL environments through service personalization. Section 2 presents related work within user modeling and service personalization. The third section presents the Ambient Assistive Technology User Model (AATUM) ontology and its structure, highlighting the main covered aspects and describing its functionality. Then, in the fourth section, two use cases are presented showing real life situations; these are used in the fifth section in order to demonstrate the ontology usage. The last section includes conclusions and future research work.

Related Work

As mentioned before, one of the core aspects in service personalization is user modeling. Ontology-based user modeling has been previously proposed in many research areas like knowledge management systems [START_REF] Razmerita | Ontology-based user modeling for knowledge management systems[END_REF], semantic web search [START_REF] Jiang | Learning and inferencing in user ontology for personalized semantic web search[END_REF] and digital museum guides [START_REF] Hatala | Ontology-based user modeling in an augmented audio reality system for museums[END_REF]. The increasing attention of ontological modeling is mostly due to its interoperability feature and ability to enable knowledge sharing and reuse over several application domains [START_REF] Heckmann | Gumo-the general user model ontology[END_REF].

One important issue is that user preference and needs may change depending on the user context. Thus, the system has to be able to infer which context the user is in and consequently adapt the ambient to provide the appropriate assistance. The UPOS (User Profile Ontology with Situation-Dependent Preferences Support) [START_REF] Sutterer | Upos: User profile ontology with situationdependent preferences support[END_REF] introduced the concept of dynamic user profiles. The ontology supports the creation of a subset of conditional user profiles associated with the user context. According to a condition (e.g. if the context of user Bob equals the My-Office location), the matching process tries to find the correspondent sub-profile. If a match happens, the found user profile is applied for service personalization.

Another relevant concern within AAL service personalization is the need of having information about the user's health condition and his/her limitations performing daily activities. Without the correct representation of the user´s needs and capabilities, it´s unlikely that the ambient will properly adapt itself to provide optimum assistance for the elderly and for people with special requirements. R. Kadouche et al. [START_REF] Kadouche | Personalization in smart homes for disabled people[END_REF] proposed the Semantic Matching Framework (SMF) capable of providing an appropriate middleware for delivering personalized assistive services according to the user's needs and capabilities. The main feature of SMF is based on the semantic matching between the user model and the environment model. The user model describes user information, preferences and capabilities while the environment model defines the available devices (e.g. door) and their attributes (e.g. required force to open the door). Using a reasoning mechanism, the SMF analyzes user capabilities and the environment and deduces the "handicap situation" in order to deliver personalized services.

The PCEICL (Person Centered Environment for Information, Communication and Learning) [START_REF] Fredrich | An ontology for user profile modelling in the field of ambient assisted living[END_REF] platform aims to offer a better assistance to elderly people using context aware and personalizable services. They have proposed an ontology where the user is the central concept and is described by their characteristics such as their health condition, capabilities and preferences. In order to have an exact and correct description of the user´s health condition, they have used the International Code for Diseases (ICD) [START_REF] Organization | International classification of diseases (icd)[END_REF].

Another approach of service personalization in the field of AAL is the Mo-bileSage [START_REF] Skillen | Ontological user profile modeling for context-aware application personalization[END_REF]. The main purpose of their work is to provide help on-demand services as the user moves between mobile environments. Based on the user's characteristics and his/her location, the system can personalize services in order to assist the user in his/her daily activities like outdoor navigation and the use of devices such as ticket vending machines. As in [START_REF] Fredrich | An ontology for user profile modelling in the field of ambient assisted living[END_REF], MobileSage ontology models the user as a central concept of the system as well as his/her environment. The user profile is composed by a set of sub profiles like a capability profile, a health profile and an interest profile.

The main issue of the aforementioned works is the lack of a uniform and consistent representation of user health condition, functioning and disability. The representation of this information is usually designed in order to meet the requirements of a specific application. Thus, the main feature of using an ontology, i.e. the knowledge sharing and reuse, is not fully utilized.

The AATUM ontology

In order to prevent common mistakes and make the best modeling decisions while developing the ontology, we have taken into account the design method proposed by [START_REF] Noy | Ontology development 101: A guide to creating your first ontology[END_REF]. Using a traditional top-down approach, both static and dynamic highlevel concepts related to the user were selected and further broken down into specialized concepts. The AATUM ontology has been implemented in OWL, the Ontology Web Language that is a xml-based semantic web language proposed by the World Wide Web Consortium (W3C). To help with the process of creating, editing and viewing the ontology, the Protégé-OWL Editor1 was selected. A brief explanation of the ontology main classes is depicted in Table 1. To illustrate the ontological structure and the relationship between its classes, a graphical representation is presented in Fig. 1. Basic information such as address, date of birth, telephone number and family contacts is stored in the class PersonalInfo. Though this information may not seem to be very useful, it could be used for important purposes in terms of ALL. For example, this information could be used to send an ambulance to a user's house after a heart attack or in a statistical report documenting the health conditions of a neighborhood's residents.

The class Interest holds information about personal interests related either to a hobby or work. Every interest has a weight associated in order to measure how much the user is interested in that specific subject. Moreover, additional information like descriptions or schedules can be stored. This class is useful for recommendations or content-filtering applications and can help people to have a higher quality of life. For example, the task of choosing a movie on television would be much easier for an elderly person if only desirable options were presented.

Extent Of Impairment

The degree of the impairment of function or structure "Mild impairment", "Severe impairment"

Activities and Participation

Difficulties the user may have in executing activities or in involvement in life situations "Walking", "Reading", "Relating with strangers"

Capacity Level

Individual's ability to execute a task or an action "Mild difficulty", "Severe difficulty"

The class Context is used to represent user's context such as the location, the time, and the activity the user is performing. One key advantage of defining the context this way is the possibility of inferring additional information from a small amount of sensor data. For example, using only the information that the user is located in his bedroom and it is 01:00 AM, the system can infer that the user is sleeping and then adapt the ambient in order to give the user a better night sleep.

The user's behavior and preferences depend on the temporal and environmental context the user is in. For example, the user's smartphone should be set to silent mode during a meeting and to loud mode when the user is at home; the shower water temperature is likely to be higher in the winter compared to the summer; the desired ambient luminosity may be set to high in the evening and to none during sleep time. Thus, it's crucial to have different profiles related to different contexts. This is done through the class ConditionalUserProfile that is linked to the class Context. The preferences that are unlikely to change according to the context are linked to a default profile represented by the class UserProfile, which is the superclass of ConditionalUserProfile .

The most important concepts of the ontology are the classes related to the user's health condition and capabilities. Having a complete, uniform, and consistent model of the user's functioning and disability levels allows correct service tailoring, and thus a better quality of life for impaired and elderly people.

Information about user health condition, i.e, the disease or disorder diagnosis is stored in HealthCondition class. As in [START_REF] Fredrich | An ontology for user profile modelling in the field of ambient assisted living[END_REF], this information is composed by the disease/disorder level, its related medication, and its ICD , which is a worldwide used code. Also, additional information relevant to medical accompaniment or treatment can be stored. This information could be used, for instance, to give an analysis of the general health situation of a population group or to prompt the user about his/her medication schedule.

According to [START_REF] Organization | International classification of functioning, disability and health: ICF[END_REF], diagnosis of a disease or disorder by itself does not predict service needs, length of hospitalizations, level of care, or functional outcomes. If a person cannot perform an activity it may be related to any of various different health conditions. In other words, it is very hard to infer participation in everyday life from medical diagnosis alone. This implies that without data about levels of functioning and disability, we will not have the information needed to properly assist the user in his daily activities. Therefore, we used The International Classification of Functioning, Disability and Health (ICF) to model the user's functioning and disability levels in a consistent and internationally comparable way. An excerpt of the class describing user impairments is shown in Fig. 2 while Fig. 3 presents an excerpt of the class that describes user limitations performing activities and participation restrictions.

We also have used the ICF qualifiers to record the presence and severity of a problem in functioning at the body, person and societal levels. For the classifications of body function and structure, the qualifier ExtentOfImpairment indicates, on a five point scale, the degree of the impairment of function or structure. The possible values are: no impairment, mild, moderate, severe and complete. In the case of the Activity and Participation list of domains, the Capacity qualifier describes an individual's ability to execute a task or an action using the same five point scale.

Use case study

Based on the elderly and people with functional diversity most important requirements presented in [START_REF] Rusu | A conceptual approach for innovative home care solution[END_REF] and [START_REF] De Ruyter | Ambient assisted living research in the carelab[END_REF], two use cases where the ontology can be used in order to properly assist the user to perform his/her activities of daily living were defined. First, a short description of the users is given:

Mr. John: Mr. John is a 63 year old retired Professor living alone is his apartment. Though he left his job recently, he still reads scientific news on his personal computer or tablet. He started to cook as a hobby and a few weeks ago he started to follow a foreign documentary about Asian cuisine that is broadcast every Wednesday night. He has a high level of myopia which makes it hard to read small or distant texts.

Mr. Noel: Mr. Noel is a 81 year old widower living with his daughter. Because he suffers from cardiac arrhythmia, his heart rate needs to be checked constantly. His daughter used to assist him with the daily care needs such as giving the medicines and checking his heart rate, but since she got a new job, Mr. Noel will have to stay by himself during weekday afternoons.

Use case 1 : Every Wednesday night the system will show a notification in Mr. John's smartphone telling him that the documentary is about to start. Moreover, additional information about the specific episode is shown. If Mr. John confirms he's going to watch the documentary, the system will turn on the TV, switch to the correct channel, set the subtitles to English and adjust its size in order to make it possible for Mr John to read it comfortably. Also, the room lights are turned off.

Use case 2 : While Mr. Noel is by himself at home, his heart rate is obtained by a wearable sensor and transmitted wirelessly to the system. This data is compared with values determined safe by his doctor, and in case of an emergency, both his daughter and medical staff are notified. Since Mr. Noel takes two different medications, the system attends to his medicine schedule and prompts him when medication is required. This is done through the closest electronic device, such as the living room television or his personal computer.

Ontology usage

Once we have the user model ontology, we need a infrastructure capable of delivering customizable services available in the ambient. Fig. 4 presents an overview of a service-oriented architecture (SOA) within a smart home that aims to assist the user with special requirements to have a safe and independent lifestyle using a combination of context-awareness, user modeling and service personalization. This architecture is part of our ongoing research and will be further discussed in future papers.

The data needed for populating the ontological user model is gathered in several ways. Context invariant data such as personal information, interests and health condition is acquired during the system initialization by the user or the caregiver. On the other hand, information such as preferences can be deduced from previously given information. For example, if the user has a mild hearing impairment, his preference for volume level should automatically be set to high.

Specifically for collecting the health and disability information, the system can use one of the two application instruments proposed by the World Health Organization (WHO). This is another compelling benefit of using the ICF as part of the ontology. The first one is a checklist with the most relevant ICF categories which allows the identification and qualifications of the individuals functioning profile in a straightforward manner. The second one, named WHODAS (WHO Disability Assessment Schedule), is a generic assessment instrument designed from a comprehensive set of the ICF items that are sufficiently reliable and precise for providing a standardized method for measuring health and disability across different cultures [START_REF] Üstün | Measuring health and disability: manual for WHO disability assessment schedule WHODAS 2.0[END_REF]. A unique feature of WHODAS, that distinguishes it from other disability measures, is its direct association to the ICF. According to the WHO, the WHODAS 12-item version has an average interview time of only five minutes, what it makes it a very affordable strategy to collect all necessary user's health and disability information.

The next subsections depict how the proposed AATUM ontology and the system architecture are used to provide user optimal assistance with the use cases introduced in Section 4.

Use case 1

Mr. John's interest about the Asian cuisine documentary is stored as an instance of the class Interest and the documentary's hours and channel is saved as the class's property AdditionalInformation.

Knowing the current day and time, the system searches on the Internet additional information about the episode and sends to John's smartphone. After Mr. John confirms he's going to watch the episode, the living room television is turned on and set to the documentary's channel.

Using the information about his seeing impairment stored as an instance of the ICF class b210. Seeing along his context information Watching TV, the system infers the preference Subtitle size: large and saves it as an instance of the class Preference that is linked to his conditional profile John WatchingTvProfile.

In the last times Mr. John watched TV, he turned off the room's lights. This pattern was learned by the system reasoner using a predefined rule and stored as the preference Room lightning: dark that is also linked to his conditional profile John WatchingTvProfile.

An excerpt of the ontology classes instances describing this use case is presented in Fig. 5.

Use case 2

Mr. Noel's heart disease is stored as an instance of the class HealthCondition, as it's ICD code (I49.9) and medication schedule. The heart rate values determined safe by his doctor are stored as the class' property AdditionalInformation. His daughter's and hospital's telephone number, as his address, are saved in the class PersonalInfo. This way, when his body sensor detect unsafe values, the system sends a text message notifying his daughter and calls an ambulance to his house. After attending his medicine schedule, the system determines the device where the notification should be displayed using his context information stored in Location, that was obtained through presence sensors. An excerpt of the ontology classes instances describing this use case is presented in Fig. 6.

Conclusion

In this paper we have presented the AATUM, a novel ontology for user modeling in the field of AAL. We have demonstrated, through two case studies, how the proposed ontology is used to properly assist the elderly with their activities daily living in a smart home, achieving a safe and independent lifestyle.

The use of ontologies for user modeling within AAL is not new, but the related works fail in the representation of user health condition, functioning, and disability, which are essential components to properly provide optimum assistance for the elderly and for people with special requirements. In the AATUM ontology, the user is the central concept and is described by his/her static and dynamic properties such as personal information, interests, health condition, etc. The AATUM ontology main feature is the use of the ICF, the World Health Organization's framework for health and disability, to model the user's functioning and disability levels in a consistent and internationally comparable way. Also, the ICD code is used to properly describe the disease or disorder diagnosis. Another compelling feature is the use of a conditional user profile related to the user's context to describe situation-dependent preferences.

Future work will aim to develop the reasoning mechanism to provide personalized services according to the user profile described by the AATUM ontology and his/her context. Further evaluation will involve the total implementation and integration of the service personalization component with a smart home

Fig. 1 .

 1 Fig. 1. An overview of the AATUM ontological structure

Fig. 2 .Fig. 3 .

 23 Fig. 2. An excerpt of the Impairment class as shown within Protégé

Fig. 4 .

 4 Fig. 4. System architecture for service personalization in a smart home

Fig. 5 .

 5 Fig. 5. Ontology classes instances for Use Case 1

Fig. 6 .

 6 Fig. 6. Ontology classes instances for Use Case 2

Table 1 .

 1 AATUM ontology main classes

	Concept	Description	Example Values
	User	The user of the system	"User John"
	User Profile	Default profile associated to preferences of one particular user	"John DefaultProfile"
	User Conditional Profile	Conditional profile associated to the user's context describing situation-dependent preferences.	"John SleepingProfile", "John WeekendsProfile", "Noel LivingRoomProfile"
	Context	Environmental information re-lated with the user such as lo-cation, time or activity	"Sleeping", "In the kitchen", "Evening"
	Personal Info	Basic user information like ad-dress, contacts, age and e-mail	"59 Homewood st." "37 year old", "Son's Tel.: 800-876-5380"
	Interest	Hobbies or work-related interests	"Cooking", "Hockey", "Science news"
	Preference	Individual preferences related to a service	"Room temperature = 75 °F", "Text size = LARGE", "Pre-ferred media = AUDIO"
	Health Condition	A disorder, disease or injury di-agnosis	"Cerebral palsy", "Back pain", "Diabets"
	Medication	Medication used in the disorder, disease or injury treatment	"Lisinopril', "Hydrocodone"	"Simvastatin",
		Problems in body function and	"Pancreatic	dysfunction",
	Impairment	structure such as significant de-	"Respiratory	dysfunction",
		viation or loss	"Reduced mobility joint"

Protégé-OWL Editor: Available at http://protege.stanford.edu/

Acknowledgment. This research work has been funded by the CAPES PROCAD project (071/2013), whose support is gratefully acknowledged.

based on a service-oriented and context-aware architecture.


Andrés Goens
email: andres.goens@tu-dresden.de

Jeronimo Castrillon
email: jeronimo.castrillon@tu-dresden.de

Analysis of Process Traces for Mapping Dynamic KPN Applications to MPSoCs

Current approaches for mapping Kahn Process Networks (KPN) and Dynamic Data Flow (DDF) applications rely on assumptions on the program behavior specific to an execution. Thus, a near-optimal mapping, computed for a given input data set, may become sub-optimal at run-time. This happens when a different data set induces a significantly different behavior. We address this problem by leveraging inherent mathematical structures of the dataflow models and the hardware architectures. On the side of the dataflow models, we rely on the monoid structure of histories and traces. This structure help us formalize the behavior of multiple executions of a given dynamic application. By defining metrics we have a formal framework for comparing the executions. On the side of the hardware, we take advantage of symmetries in the architecture to reduce the search space for the mapping problem. We evaluate our implementation on execution variations of a randomly-generated KPN application and on a low-variation JPEG encoder benchmark. Using the described methods we show that trace differences are not sufficient for characterizing performance losses. Additionally, using platform symmetries we manage to reduce the design space in the experiments by two orders of magnitude.

Introduction

Architecture trends show a growing number of processors and heterogeneity in embedded systems. The problem of leveraging the growing complexity of modern multi-processor systems-on-chip (MPSoCs) is as relevant as ever. In many application domains it is well-established to use programming abstractions such as Kahn Process Networks (KPN) [START_REF] Gilles | The semantics of a simple language for parallel programming[END_REF] or actor-based data flow models like Synchronous Data Flow (SDF) [START_REF] Lee | Synchronous data flow[END_REF] and dynamic data flow (DDF) [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF] for describing applications. These abstractions allow synthesis tools to reason on a high-level about physical resource allocation within the chip. They model the application by using a directed graph, where so-called actors or processes, represented by the nodes in the graph, communicate with each other via channels, which are in turn represented by edges. Much work has been done regarding the problem of mapping KPN and data flow applications to complex hardware architectures for optimal throughput, resource usage or energy-efficiency [START_REF] Singh | Mapping on multi/many-core systems: survey of current and emerging trends[END_REF]. The heuristics used for this, however, rely on a well-defined program behavior. In the case of SDF applications, for example, the very nature of the model allows synthesis tools to reason about mapping by using a topology matrix and finding repetition vectors in its kernel, which fully describe the communication behavior between actors [START_REF] Lee | Synchronous data flow[END_REF]. Finding near-optimal solutions in more general models, which do not have constraints on the program behavior as strong as those of SDF, is a much more complex task. There are several current approaches to static mapping [START_REF] Castrillon | Communication-Aware Mapping of KPN Applications onto Heterogeneous MPSoCs[END_REF][START_REF] Pimentel | A systematic approach to exploring embedded system architectures at multiple abstraction levels[END_REF][START_REF] Thiele | Mapping applications to tiled multiprocessor embedded systems[END_REF][START_REF] Castrillon | Communication-Aware Mapping of KPN Applications onto Heterogeneous MPSoCs[END_REF]. All these approaches are sensitive to the selection of the input stimuli that induce the observed trace. To deal with multiple different executions, authors suggest to compute a mapping for every situation and then pick the best configuration. For example, for buffer sizing, one approach is to select the largest size across all configurations [START_REF] Brunet | Analysis and optimization of dynamic dataflow programs[END_REF]. An alternative to deal with variations is to use the so-called real-time calculus [START_REF] Thiele | Real-time calculus for scheduling hard real-time systems[END_REF], in which events are modeled by arrival curves that describe upper and lower bounds on the event rates.

In this paper we seek to improve the current state of trace-based mapping flows to better support multiple traces for one application. We do this in two ways: by using trace theory, defining metrics in order to compare application traces and by using group theory to describe and utilize symmetries in the architecture. Trace theory has been a well-established model for concurrency for decades since its first formal formulation in 1977 by Mazurkiewicz [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretations[END_REF]. Metrics for traces have been defined in very different contexts [START_REF] De Bakker | Denotational semantics of concurrency[END_REF], or for similar applications very specific metrics have been considered [START_REF] Kengne | Distancebased trace diagnosis for multimedia applications: Help me ted! In Semantic Computing[END_REF]. To the best of our knowledge, however, trace metrics have never been used in the general context of analyzing KPN processes.

Process Traces and Histories

In this section we present our proposed trace analysis methods for the application side. To this end we introduce the formal concepts of traces and histories, explain their relationship and define a metric on the space of traces and of histories. We then describe experimental results obtained by applying these methods to randomly-generated KPN traces and on a JPEG encoder.

Traces and Histories

Traces and histories are both generalizations of strings. They are well-known as models for concurrently executing processes. Informally, we model concurrently executing processes as a string over an alphabet Σ, where the words of the alphabet represent events of the system. In a regular string all occurring characters (or events) have a well-defined sequential ordering. When two contiguous characters, however, represent independent events in the system, then we do not distinguish their order in the trace: we consider two traces as equal when we can convert one to the other by just rearranging independent characters. More formally, let Σ 1 , . . . , Σ n be n alphabets, and consider the alphabet Σ " Σ 1 Y . . . Y Σ n , the union of those alphabets. This union is not necessarily disjoint. We define a dependence subset D of Σ 2 by D " Σ 2 1 Y . . . Y Σ 2 n . From this we define the set I " Σ 2 zD. It can be used to define an equivalence relation " on the set of strings Σ ˚. We say that ab " ba, if and only if pa, bq P I. This induces an equivalence relation " on Σ ˚by extending it to all strings (the reflexive, transitive symmetric closure). We define the set of traces as the factor set of equivalence classes Σ ˚{ ". Since strings with concatenation have the algebraic structure of a monoid, and concatenation and the epimorphism to the equivalence class " commute, Σ ˚{ " is also a monoid with concatenation. It is therefore usually called the trace monoid [START_REF] Diekert | The book of traces[END_REF].

Histories are similar. Instead of an arbitrary concatenation of the various independent strings, we consider a history to be a tuple of strings, one in each of the alphabets Σ i . The individual alphabets represent the possible events for individual processes. These alphabets can have some common characters between them, in which case Σ i X Σ j ‰ H holds. These common characters represent synchronization events: they happen in two or more processes at the same time.

We can think of a history as a log of an application which represents all events in a parallel execution with different tasks or processes. The projection onto the alphabet of a single process represents the individual history of that process, independent of the others. With respect to component-wise concatenation, the set of histories over the alphabet Σ " Σ 1 Y . . . Y Σ n is also a monoid, which is why it is often called the history monoid [START_REF] Diekert | The book of traces[END_REF].

These two structures, the trace and the history monoid, are isomorphic. We either list events sequentially in a trace, where we don't distinguish the order of independent events, or we define the sequential history of each process independently. A formal proof of this fact can be found in [START_REF] Diekert | The book of traces[END_REF].

Metrics

A metric acts as a way of measuring distance between objects. If we consider traces and histories as descriptions of the behavior of individual executions of a software built of concurrent processes, a metric acts as a way of comparing said execution behaviors.

There exists a plethora of metrics on strings, which are used from coding theory to DNA analysis and approximate string matching. Notable examples include the Hamming distance which only counts the number of equal letters, or the edit distance, which counts the minimal number of deletions, insertions and substitutions needed to go from one string to another. We can generalize these metrics to histories (and thus, traces) with the following theorem:

Theorem 1. Let Σ " Σ 1 Y . . . Y Σ n be
an alphabet and d be a metric on the strings Σ ˚over Σ. Then d induces a metric d on the set of histories H over pΣ 1 , . . . , Σ n q with projections π 1 , . . . , π n by dpx " px 1 , . . . , x n q, y " py 1 , . . . , y n qq "

n ÿ i"1 dpx i , y i q " n ÿ i"1 dpπ i pxq, π i pyqq (1)
Proof. Let x, y, z P H be histories.

1. Let dpx, yq " 0. Then dpπ i pxq, π i pyqq " 0 for all i " 1, . . . , n. Since d is a metric, it means that π i pxq " π i pyq for all i. This implies that x " y since it holds for all projections. 2. By definition (Eqn. 1) it is immediately obvious that, since d is a metric dpx, yq "

n ÿ i"1 dpπ i pxq, π i pyqq " n ÿ i"1 dpπ i pyq, π i pxqq " dpy, xq 3.
Finally, the triangle equation also follows in a similar fashion:

dpx, yq " n ÿ i"1 dpπ i pxq, π i pyqq looooooomooooooon ďdpπipxq,πipzqq`dpπipzq,πipyqq ď n ÿ i"1 dpπ i pxq, π i pzqq `dpπ i pzq, π i pyqq " n ÿ i"1 dpπ i pxq, π i pzqq `n ÿ i"1 dpπ i pzq, π i pyqq " dpx, zq `dpz, yq
Similar to this construction, and inspired by the l p norms, we can define other metrics on histories (and traces).

Let p P R ě1 be a real number, greater than or equal to one. Further let Σ " Σ 1 Y . . . Y Σ n be a history alphabet and let

d 1 i : Σ i Ñ R ě0 be a metric on Σ i , i " 1, . . . , n. Let H Ď Σ 1 ˆ.
. . ˆΣn be the set of histories on Σ, with the corresponding projections π i : H Ñ Σ i , i " 1, . . . , n. We call the mapping

d p : H ˆH Ñ R ě0 , px, yq Þ Ñ p g f f e n ÿ i"1 d 1 i pπ i pxq, π i pyqq p
the p-metric on the histories. Similarly, we can define a 8 metric d 8 as d 8 px, yq " max i"1,..., dpπ i pxq, π i pyqq. The proof that these induce metrics is very similar to that of Theorem 1.

Trace analysis

To have controlled differences in our traces, we use random KPN traces. We generate them with a modification of the open-source software tool sdf 3 [START_REF] Stuijk | SDF 3 : SDF For Free[END_REF]. Concretely, we generate a random SDF application, and subsequently modify it to have a less static behavior. We do this by generating a set of possible, different input/output behaviors and randomly varying between them at runtime. For realistic behavior, we do this only on some KPN processes, while others keep their static (SDF) behavior. This method is inspired by the random KPN generation described in [START_REF] Castrillon | Programming Heterogeneous MPSoCs: Tool Flows to Close the Software Productivity Gap[END_REF]. Once the application has been generated, different traces are created. This is achieved by fixing the possible behaviors and only randomizing the frequencies of occurrence.

For evaluating mappings we use a discrete-event-simulator similar to the one described in [START_REF] Castrillon | Maps: Mapping concurrent dataflow applications to heterogeneous mpsocs[END_REF]. As the target architecture we use a virtual platform, also similar Fig. 1: A diagram of the test architecture used to the one described in [START_REF] Castrillon | Maps: Mapping concurrent dataflow applications to heterogeneous mpsocs[END_REF]. It has two identical RISC (ARM) processors and four identical vector DSPs. A diagram of this test architecture can be seen in Figure 1.

For evaluating the methods proposed in this section we used a fixed, randomly generated process network which had four different processes and four FIFO channels. We generated 1000 different random process traces of diverse lengths and behaviors. For each of these 1000 traces we calculated the optimal mapping by using the discrete event simulator and exhaustively evaluating all 6 4 " 1296 different possible (process-to-processor) mappings. For buffer sizing we used a simple strategy assigning the same size to the buffers on all traces for an accurate comparison. This approach is inefficient and time-consuming, but only by using truly optimal mappings can we achieve a valid analysis. Without the optimality of the mapping there is no guarantee that it is good for a trace, even if it was specifically calculated for it.

Random traces provide only limited insight into this problem. To validate our approach we also considered a JPEG encoder with an existing implementation as a KPN. The JPEG encoder needs to perform run-length encoding, which exhibits dynamic behavior for the KPN channels. We executed the JPEG encoder on a benchmark consisting of 200 images adapted from the BSDS500 Benchmark [START_REF] Arbelaez | Contour detection and hierarchical image segmentation[END_REF].

The exponential scaling of the exhaustive mapping evaluation is also the reason why a network with only four processes was chosen for the random traces. For larger applications where the problem size makes exhaustive evaluation prohibitively long, as is the case for the JPEG encoder, good meta-heuristics like evolutionary algorithms can be considered as a replacement. While this does not guarantee the same accuracy for the comparison, using the results of a good meta-heuristic should produce a solid basis for comparison nevertheless. For the JPEG encoder we use simple heuristics from the literature (e.g., load balancing).

Results

We chose a reference trace for comparing. Then, for each of the 1000 random traces we compared the optimal run-time obtained using the optimal mapping with the run-time obtained using the reference mapping (in general only optimal for the reference trace). From the quotient of both we obtained a slowdown factor ě 1. Similarly, we calculated the distance between each trace and the reference one. Using this we analyze the correlation between trace distance and the slowdown from using the sub-optimal mapping. The results can be seen in Figure 2. This figure uses three different induced metrics from two string metrics for a total of six metrics. They have been normalized to one within the data-set for comparison. The axes on Figure 2b were adjusted not to show the trivial points at p0, 1q (for the reference trace). This is for the sole purpose of a better visual scaling of the plot. As an example, consider the point marked in Figure 2a. This point has the coordinates p0.24, 1.42q. It means that the distance between the trace corresponding to the point, and the reference trace was 24% of the maximal distance in the plot (concretely, d 1 " 101 with a maximal distance of 424). The 1.42 slowdown factor means that the execution time of the trace with the reference mapping was 42% slower than with its own optimal mapping. Altogether, Figure 2 shows a low correlation between the trace distance and how good the mapping of one trace is for the other one. Concretely, the correlation coefficients are ´0.014, ´0.077, ´0.095, 0.119, 0.010, and ´0.059, for the d 1 , d 2 and d 8 norms induced by the edit and Hamming distances, in that order.

JPEG Encoder

Figure 4 shows a histogram of different trace metrics for the 200 JPEG encoder executions. The traces were normalized with the distance from the reference trace to the empty trace, to give an idea of how much variation was between the traces. The JPEG encoder has variation in traces due to the run-length encoder, which is a small function that sends a different amount of tokens depending on the compressed data. However, the majority of the computation time is due to the discrete cosine transform, which has a static behavior. Even though the run-length encoder represents just a small fraction of the computation, we found performance and trace behavior deviations. By using the mapping tailored for a different trace, a slowdown of up to 1.77% was observed. More importantly though, we see that different inputs yield different behaviors, represented by different traces. We also see that these differences have a negative impact on performance, albeit a small one in this case. In the future we plan to investigate further applications where the dynamic data flow part of the application amounts to a more significant percentage of the execution.

Permutations of Mappings

From the trace analysis above we see that distance analysis itself does not suffice to infer the performance of different mappings. Instead, in this section we consider the problem from the perspective of the mappings and the architecture, as opposed to that of the traces and the application. We take advantage of the fact that heterogeneous platforms have some degree of symmetry. We formally define and explore this symmetry, and present a strategy to reduce the design space that leverages it.

Problem Formulation

Mathematically, we can formulate our problem as follows: Let P be a set of physical resources (e.g. processing elements, on-chip memories) and let L be a set representing logical elements (e.g., processes, FIFO channels). We define a valid mapping m : L Ñ P as a mapping in the mathematical sense (a function), such that it respects the KPN structure. Formally, let G be a subgroup of the symmetric group of the physical resources S P . The canonical action of the group G on P induces an action on the set of mappings m : L Ñ P : for g P G and m : L Ñ P a mapping, i.e. pg¨mqplq :" g¨mplq for all l P L. We require of a symmetry group that the run-time for all traces is an invariant of the group action. In particular, this means that the action of G on the set of mappings restricts to an action on the set of valid mappings. This implies, for example, that we only consider symmetries of the architecture that map processors to processors and communication resources to equivalent communication resources. We define equivalence classes for mappings: we say two mappings m, m 1 are equivalent if there exists a symmetry of the architecture g P G such that g ¨m " m 1 , i.e., if m and m 1 are in the same orbit under the action induced by G on the set of valid mappings.

For example, let P " tRISC 1 , RISC 2 , DSP 1 , . . . , DSP 4 u be the processor set of the architecture from the experimental setup in last section (see Figure 1), and let L " tp 1 , . . . , p 4 u be the process set of the four-process KPN used in the example from last section. For simplicity, we consider an elementary, symmetric communication model in this example where communication resources and processors are coupled. Then the group G that can swap both RISC processors and allows any permutation of the four DSP processors is the symmetry group of this architecture. It is isomorphic to S 2 ˆS4 , i.e., the direct product of the symmetric groups on two and four elements respectively. As an example, consider the mappings

m 1 : p 1 Þ Ñ RISC 1 , p 2 , p 3 Þ Ñ DSP 2 , p 4 Þ Ñ DSP 3 m 2 : p 1 Þ Ñ RISC 1 , p 2 , p 3 Þ Ñ DSP 1 , p 4 Þ Ñ DSP 4 m 3 : p 1 Þ Ñ RISC 1 , p 2 , p 4 Þ Ñ DSP 2 , p 3 Þ Ñ DSP 3 .
Then, m 1 and m 2 are equivalent, however neither of them is equivalent to m 3 .

The motivation for this definition of equivalence is that if two processors are equal, then it usually should make no difference if one or the other is chosen for the mapping. This can also be used for taking communication into account, for example when there is additional symmetry from multiple memories or differences in local memories break the processor symmetry.

Groups with this structure are by far the most common symmetry group for heterogeneous architectures. A heterogeneous architecture which has n 1 equivalent processing elements of type 1, n 2 equivalent processing elements of type 2, and so forth, will have a symmetry group isomorphic to S n1 ˆSn2 ˆ¨¨¨. However, the symmetry group of a subset of equivalent processing elements need not be a full symmetric group. For example, consider a simple homogeneous four-core architecture with a Network-on-Chip (NoC), such that the communication latency between adjacent processors is considerably lower than to non-adjacent ones. Then the adjacency of the processors should be kept with any symmetry transformation, which means the symmetry group is a dihedral group of a regular polygon with 4 sides, instead of the full symmetric group on 4 points. This group is called D 4 , though some references call it D 8 because it has 8 elements. Figure 3 shows a schematic of this symmetry and an example of an allowed symmetry, one of the two generators, and a permutation that is not a symmetry of the architecture. It depicts the symmetry transformations with the green or red arrows, and an example of the action on a mapping of four processes, represented by the green or red circles.

Algorithmic Considerations

To identify equivalent mappings we need to find out if two elements are in the same orbit. Specifically, if m, m 1 are mappings, we need to test if m 1 P Gm. This can in general be done with Op|Gm||S|q group element applications, where |S| is a generating set of the group G, see Theorem 2.1.1 of [START_REF] Seress | Permutation group algorithms[END_REF]. Since we do not plan to deal with very complex symmetry groups, however, we used a different approach. Our approach is tailored for groups that have the form Ś k i"1 S ni , for n 1 , . . . , n k P N. It takes advantage of the fact that group membership testing is a simple task in groups of this family. We devised a strategy that given mappings m, m 1 generates a tentative mapping σ : t1, . . . , |P |u Ñ t1, . . . , |P |u such that if there exists a τ P S |P | such that τ ¨m " m 1 , then σ is a permutation and it holds that σ ¨m " m 1 . We achieve this by iterating over all elements e in the definition domain of mapping m and updating σ to be correct for that element Algorithm 1 is more efficient than the standard algorithm. It uses a constant, single group application instead of Op|Gm||S|q. However, it relies on the fact that if the proposed element σ is not in G, then there exists no element g P G mapping m to m 1 , which is by no means obvious if G is not of the form Ś k i"1 S ni . For the general case, the standard black-box group algorithms should be used (see [START_REF] Seress | Permutation group algorithms[END_REF]).

The permutation approach has limited scalability. Using Burnside's Lemma [START_REF] Burnside | Theory of groups of finite order[END_REF], it is straightforward to prove that the factor by which the size of the search space is reduced is bounded by the cardinality of the symmetry group. In partic-ular, the asymptotic scaling behavior of the size of the search space is the same, it still is in Op|P | |L| q. However, we see in the experiments in the next section that not all equivalence classes of mappings are equally common. Further investigation could concentrate on identifying the most important equivalence classes and their corresponding traces.

Experimental results

For evaluating this approach, we used the same basic setup as in Section 2. Using Algorithm 1 we identified equivalence classes in the optimal-run-time mappings of the same set of 1000 random process from Section 2. We selected one trace and identified all traces which yielded mappings equivalent to it. In general, for a system with 6 processors total where there are two groups of 4 and 2 equivalent processors respectively, there exist exactly 83 possible mappings of four processes. This fact can be verified using Burnside's Lemma. Out of the 1000 traces a total 23 were equivalent to the first one. They all had a slowdown factor of exactly 1, as would be expected of equivalent mappings. This is, however, only a fraction of the 161 mappings with a slowdown factor of 1 compared to the first trace.

Furthermore, of all 83 possible mappings, considering symmetry, only 30 were present in the traces. Figure 5 shows a bar plot of the percentage of traces belonging to each group, for the 30 groups up to symmetry which had a trace with an optimal mapping in this group. They are ordered from most common to least common, and the remaining 53 unrepresented groups are not depicted.

This results show that while there are quite a few possible equivalence classes of mappings, 83 in this case, only very few are actually good mappings. The two most common equivalence classes are optimal for almost 30% of the traces, while the five most common ones actually account for more than half the traces.

The JPEG encoder was not considered for this since it would be too computationally intensive to calculate optimal mappings, and it would have yielded limited insight for the lack of optimality variations between traces. In this paper we have considered the differences in execution behaviors of KPN and dynamic data flow applications as process traces or histories. We defined a metric space structure on traces and used it to measure the relationship between the trace distance, and how good the optimal mapping of one trace works for the other. For this, we also developed a framework for comparing them, which included exhaustive search on small examples to find true optimal mappings, for a solid comparison base.

The results from the JPEG encoder showed behavioral variations for different inputs in a real application. Additionally, the results from our analysis on random traces suggest no correlation between the trace distance and the goodness of the mappings of one to the other. This is a very revealing result. Its implications are twofold. First, it means that the difference between two traces does not suffice to t if we can use the same mapping for both. In particular this means we should devise more elaborate strategies for trace grouping, probably applicationspecific ones. The second, less obvious implication, is that very small differences in traces can have a very big impact on performance. Further work will focus on real applications with more dynamic behavior than the JPEG encoder that was used.

Apart form the behavior in the form of the traces, we also considered the problem from the perspective of the mappings. We defined a strategy to leverage symmetries in the architecture and evaluated it with the experiments used for the traces. We managed to reduce the search space from 1296 possible mappings to 83 possible equivalence classes of mappings, and found that very few equivalence classes of mappings account for the optimal throughput in the majority of traces.

Another direction for future work is to define strategies for identifying traces at run-time and using trace-specific information about the optimal mapping for dynamically improving adaptive execution. The analysis framework can be used to consider the problem of buffer sizing for multiple traces, which was not addressed in this work.

Fig. 2 :

 2 Fig. 2: Application slowdown as a function of different trace distances

  (a) The generator element for the D4 symmetry (b) A permutation not included in the D4 symmetry

Fig. 3 :Algorithm 1

 31 Fig. 3: Schematic representation on of the symmetry of a 4-core NoC Architecture

Fig. 4 :Fig. 5 :

 45 Fig. 4: Histogram of normalized traces differences (JPEG encoder)

Acknowledgments

This work is supported in part by the German Research Foundation (DFG) within the Cluster of Excellence "Center for Advancing Electronics Dresden" (cfaed). We would like to thank Silexica (www.silexica.com) for making their embedded multicore software development tool suite available to us as basis for our work.