Antonio Wendell

O Rodrigues -Frédéric

'h -Jean-Luc Guyomarc

Dekeyser

O Rodrigues

Frédéric Guyomarc'h †
email: frederic.guyomarch@inria.fr

Jean-Luc Dekeyser
email: jean-luc.dekeyser@lifl.fr

An MDE Approach for Automatic Code Generation from MARTE to OpenCL

Keywords: OpenCL, GPU, Gaspard2, MDE, MARTE, UML, Automatic Code Generation

Advanced engineering and scientific communities have used parallel programming to solve their large scale complex problems. Achieving high performance is the main advantage for this choice. However, as parallel programming requires a non-trivial distribution of tasks and data, developers find it hard to implement their applications effectively. Thus, in order to reduce design complexity, we propose an approach to generate code for OpenCL API, an open standard for parallel programming of heterogeneous systems. This approach is based on Model Driven Engineering (MDE) and Modeling and Analysis of Real-Time and Embedded Systems (MARTE) standard proposed by Object Management Group (OMG). The aim is to provide resources to non-specialist in parallel programming to implement their applications. Moreover, concepts like reuse and platform independence are present. Since we have designed an application and execution platform architecture, we can reuse the same project to add more functionalities and/or change the target architecture. Consequently, this approach helps industries to achieve their time-to-market constraints. The resulting code, for the host and compute devices, are compilable source files that satisfy the specifications defined on design time.

Une Approche MDE pour la Génération Automatique de Code de Marte vers OpenCL

Résumé : L'ingénierie avancée et les communautés scientifiques utilisent souvent la programmation parallèle pour résoudre leurs problèmes complexes de grande envergure. Atteindre la haute performance est le principal avantage de ce choix. Toutefois, comme la programmation parallèle nécessite une distribution non-trivial de tâches et de données, les développeurs ont du mal à mettre en oeuvre leurs applications de manière efficace. Ainsi, afin de réduire la complexité de conception, nous proposons une approche pour générer du code pour la API OpenCL, un standard ouvert pour la programmation parallèle de systèmes hétérogènes. Cette approche est basée sur Ingénierie Dirigée par les Modèles (IDM) et de Modeling and Analysis of Real-Time and Embedded Systems (MARTE) norme proposée par l'Object Management Group (OMG). L'objectif est de fournir des ressources pour les non-spécialistes de la programmation parallèle pour dévéloper leurs applications. En outre, des concepts tels que la réutilisation et l'indépendance de plateforme sont présents. Ainsi, une fois que nous avons conçu une application et architecture de la plateforme d'exécution, nous pouvons réutiliser le même projet pour ajouter plus de fonctionnalités et/ou de modifier l'architecture cible. Par conséquent, cette approche aide les industries à atteindre leurs contraintes de time-to-market. Le code résultant, pour l'hôte et les unités de calcul, sont des fichiers source compilable qui satisfont aux spécifications définies dans la conception.

Mots-clés : OpenCL, GPU, Gaspard2, IDM, MARTE, UML, Génération Automatique de Code

Introduction

Advanced engineering and scientific communities have used parallel programming to solve their large scale complex problems for a long time. Despite the high level knowledge of the developers belonging to these communities, they find hard to implement their parallel applications effectively. Some intrinsic characteristics of parallel programming contribute to this difficulty, e.g.: race conditions, memory access bottleneck, granularity decision, thread safety, and so on. In order to make easier to program parallel applications, developers have specified several interesting programming approaches. The most currently used ones are OpenMP for shared memory and Message Passing Interface (MPI) for distributed memory programming [START_REF] Michael | Parallel Programming in C with MPI and OpenMP[END_REF]. These approaches allow to explicit and explore the parallelism of applications and architectures. Both approaches add directives with same syntax level to the target language (C, C++, Fortran). From this point of view, we can considerate this approaches are more a tool to add parallel resources to sequential programming model than a solution for parallel programming.

Recently, the consortium managed by Khronos Group released the specification to Open Computing Language (OpenCL) 1.0 [START_REF]The OpenCL Specification[END_REF]. OpenCL is the first open, royalty-free standard for general-purpose parallel programming of heterogeneous systems. It provides an uniform programming environment for software developers to write efficient, portable code for high-performance computing servers, desktop computer systems and handheld devices using a diverse mix of multicore CPUs, GPUs, Cell-type architectures and other parallel processors such as DSPs. The OpenCL has some similarities with CUDA programming model of NVIDIA.

In this paper, we propose an approach based on Model Driven Engineering (MDE) to specify, design and generate OpenCL applications. This approach relies on following aspects:

• We proposed a transformation chain in order to add or modify elements designed in a model in order to define the lower model before the code.

• The memory model of OpenCL has a distributed aspect. This approach addresses the modeling data communication and data allocation.

• Aiming to take into account the many functionalities of platform and execution models of OpenCL, an Hybrid metamodel is proposed as part of the low layer in the transformation chain.

This paper is divided into five sections. Section 2 provides a theoretical base of OpenCL and MDE necessary to next sections. Section 3 and 4 explain this approach and present a case study in order to add more resources to the work understanding. Originally, was proposed by Apple, and then turned over to the Khronos Group [START_REF]The OpenCL Specification[END_REF]. OpenCL is a standard for parallel computing consisting of a language, API, libraries and a runtime system. As depicted in figure 1, OpenCL is based on a platform model that divides a system into one host and one or several compute devices. The compute devices act as co-processors (e.g. GPUs) to the host. They are subdivided into multiple compute units (CUs), which are also subdivided into one or multiple processing elements (PEs). An OpenCL application is executed on the host, which sends instructions, defined in special functions called kernels, to the device. The OpenCL standard defines a data parallel and a task parallel programming model. In the data parallel model, the device runs multiple instances of the kernel in parallel on distinct data. Each instance is called a work-item (WI). While all work-items run the same kernel, they may perform different instructions at a time and occasionally change the instruction path (SPMD model OpenCL also defines a programming language for writing kernels, which is an extension of C. Kernels are executed within their own memory domain and may not directly access host main memory. Kernel memory is divided into four distinct regions:

HOST

• Global memory, a kind of "device main memory", can be accessed by all work-items and the host in reads/writes.

• Constant memory is similar to global memory, except that work-items may only read from this memory.

• Local memory is read/write memory local to a work-group, and is shared by all work-items of this group.

• Private memory is local to each work-item.

The OpenCL programming language defines type qualifiers to specify in which memory region a variable is stored or a pointer points to. As a kernel can neither access host main memory nor dynamically allocate global and constant memory, all memory management must be done by the host. The OpenCL API provides functions to allocate linear memory blocks in global or constant memory, as well as to copy data to or from these blocks.

Model-Driven Engineering

Model Driven Engineering (MDE) [START_REF] Lugato | Model-Driven Engineering for High Performance Computing Applications[END_REF] aims to raise the level of abstraction in program specification and increase automation in program development. The idea promoted by MDE is to use models at different levels of abstraction for developing systems, thus raising the level of abstraction in program specification. An increase of automation in program development is reached by using executable model transformations. Higher-level models are transformed into lower level models until the model can be made executable using either code generation or model interpretation.

A model is specified in some model notation or model language. Since model languages are mostly tailored to a certain domain, such a language is often called a Domain-Specific Language (DSL). A DSL can be visual or textual. A sound language description contains an abstract syntax, one or more concrete syntax descriptions, mappings between abstract and concrete syntax, and a description of the semantics. The abstract syntax of a language is often defined using a metamodel. The semantics can also be defined using a metamodel, but in most cases in practice the semantics aren't explicitly defined, they have to be derived from the runtime behavior.

A model specified using a DSL is called a Domain-Specific Model (DSM). A complex system is usually described using multiple DSMs specified in different DSLs. These models refer to each other and have to be combined when executing them. Because complex systems ask for a lot of DSMs to model them, it is important to structure the modeling space.

Applications and architectures of systems have clearly identified elements (objects) such as data parallel tasks, data dependencies, multidimensional data arrays, and architecture parts. The abstraction of each element corresponds to a concept in a model, the dependencies between these elements are represented by relationships. Models can represent abstract descriptions of these applications and facilitate their specifications and modifications because each concept and relationship are clearly identified. Moreover, views can help to represent and document models by highlighting the relevant concepts and relationships according to a particular purpose. Models are specified according to their metamodels. A metamodel gathers the set of concepts and relationships between the concepts used to describe a model, i.e., the reality according to a particular purpose (a given abstraction level for instance). Then a model conforms to a metamodel which specifies a modeling structure. In the other words, a metamodel defines the syntax of its models, like a grammar defines its language. Consequently, a metamodel can the set of necessary concepts and relationships to represent the applications and architectures of systems at a given abstraction level. A model always conforms to a metamodel. This relation is called conformance. The conformance relation has a different nature than the representation relation between a model and its system. A metamodel does not represent a model (that could be considered a system), but only the concepts and relationships that may be created.

MARTE Profile

The UML profile for MARTE (or MARTE profile) [START_REF] Omg | Modeling and Analysis of Real-time and Embedded systems (MARTE)[END_REF] extends the possibilities for modeling of application and architecture and their relations. In addition, MARTE allows extending the performance analysis and task scheduling based on target platform architecture. MARTE consists in defining foundations for model-based description of real time and embedded systems. These core concepts are then refined for both modeling and analyzing concerns. Modeling parts provide support required from specification to detailed design of real-time and embedded characteristics of systems. MARTE concerns also model-based analysis. In this perspective, the intent is not to define new techniques for analyzing real-time and embedded systems, but to support them. Hence, it provides facilities to annotate models with information required to perform specific analysis. Especially, MARTE focuses on performance and schedulability analysis. However, it defines also a general analysis framework which intends to refine/specialize any other kind of analysis. Among others, the benefits of using this profile are thus:

• providing a common way of modeling both hardware and software aspects of a RTES in order to improve communication between developers;

• enabling interoperability between development tools used for specification, design, verification, code generation, etc.;

• fostering the construction of models that may be used to make quantitative predictions regarding real-time and embedded features of systems taking into account both hardware and software characteristics.

Allocation Modeling (Alloc) from Foundations, Generic Resource Modeling (GRM) and Generic Component Model (GCM) from Design Model, and Repetitive Structure Modeling annex are packages that provide the main resources to model and to describe our entire application. In particular, RSM provides concepts to allow to express the inherent parallelism of applications.

The Repetitive Structure Modeling (RSM) annex of MARTE defines stereotypes and notations to describe in a compact way the regularity of a system's structure or topology. The structures considered are composed of repetitions of structural elements interconnected via a regular connection pattern. It provides the designer a way to express models efficiently and explicitly with a high number of identical components. The RSM is strongly inspired by the Array-OL language [START_REF] Demeure | Array-OL: Proposition d'un Formalisme Tableau pour le Traitement de Signal Multi-Dimensionnel[END_REF]. Array-OL is a graphical formalism based on array transformations which allows the full specification of the multidimensional signal processing (e.g. multidimensional data matrices). It is based on a twofold approach, known as GILR (Globally Irregular, Locally Regular): first, the global level describes the processing through a graph where the nodes exchange multidimensional arrays; second, the local level details the calculations performed on regular arrays by each node. According to MARTE, a data-parallel task T is repeated or replicated into several task instances T i,i∈1..k that take as inputs subsets of data extracted from the inputs of T , which are multidimensional arrays. These subsets of array elements are referred to as patterns or tiles.

For a given task repetition, the number k of task instances T i is given by the repetition space associated with the task T.

The tiler stereotype expresses how multidimensional arrays are tiled by patterns. When applied to a delegation connector, a tiler connects an external port with a port of an internal part. The shape of the external ports defines the shape of input/output arrays of a task. The port shape of the internal part defines the pattern shape and the shape of the part itself defines the repetition space. A tiler uses three main information to define the tiling operation:

• origin vector, which specifies the origin of the reference tile in the array;

• fitting matrix, which specifies how the patterns are filled with array elements;

• paving matrix, which specifies how an array is covered by pattern elements.

RR n°7525

Code Generation Approach

This approach proposes to generate an effective code for OpenCL and it is part of Gaspard2 [START_REF]Graphical array specification for parallel and distributed computing[END_REF] project. As described in figure 3, in design time, Gaspard2 uses UML Profile for MARTE in order to define a semantics to application project, then using transformation chains it allows us to generate code for several target platforms. One of the main advantages of MARTE is that it clearly distinguishes the hardware components from the software components. This is done via stereotypes provided in part by the Detailed Resource Modeling (DRM) package, in particular the HwResource and SwResource stereotypes. For hybrid (CPU + Compute Device) conception this separation is of prime importance as it is usual to create those two parts of the system simultaneously, by different teams. Moreover, this separation provides a flexible way to independently change the software part or the hardware part. For instance, this allows testing the software on different kind of hardware architecture, or to reuse an architecture (with a few or no changes) for different applications.

The next subsections present the conceptual models defined in design time in the Gaspard2 environment.

Design Time Models

Application

This model describes data dependencies and potential parallelism present in applications according to MARTE. The application model contains all repetitive structures, interaction ports and the communication between them. This is the application's core. Thus, we can define tasks and their interaction at data communication level. Furthermore, arrays of repetition multiplicity, expressed by stereotypes, provide information to explore task distribution onto distinct processor elements. The application conception is a very important modeling process. In fact, the developer will define three main characteristics of its application: first, which tasks and interconnection among them; second, how many times a task and its hierarchy will be executed; and third, which exchanged data and access format will be present in the application. Eventually, in order to optimize the model, an intelligent resource can perform the so-called Refactoring [START_REF] Glitia | Repetitive Model Refactoring for Design Space Exploration of Intensive Signal Processing Applications[END_REF]. It allows to find good trade-offs in the usage of storage and computation resources and in the parallelism (both task and data parallelism) exploitation.

Architecture

A platform architecture has several configuration details. However, the architecture model may be as simple as possible. For a single application, where it is not necessary to know how fast is the data access between two different memories, access time specifications may be unconsidered. Even though MARTE provides stereotypes to specify refined characteristics of platform, we need just to take into account the components and its information that will be used in allocation step. Therefore, components such as processors and memories should be modeled according to the application. Eventually, details about communication between two or more processors can help in the choice of data transfer mode.

In order to model the architecture, MARTE provides stereotypes from the Hardware Resource Modeling (HRM) from the Detailed Resource Modeling (DRM) package. In order to clearly distinguish a host from a compute device, both defined in OpenCL platform model (section 2.1), a tagged-value description in HwResource stereotype is assigned either with "Host" or with "Device" (figure 9). This is an important definition in design time because it allows to recognize kernels(section 2.1) in the application project.

Allocation

The allocation step is defined in Allocation Modeling (Alloc) from MARTE profile. Allocation of functional application parts onto the available resources (the execution architecture) is main concern of system design for specific platform. This comprehends, both spatial distribution and temporal scheduling aspects, in order to map certain operations onto available computing and communication resources and services.

Application and execution platform models are built separately, before their association through the allocation process. Often this requires prior adjustment (inside each model) to abstract/refine its components to allow a direct match.

In Gaspard2 environment, this process is a twofold action: first, we associate each designed task in application model to a designed processor in architecture model. Second, task associated flowports (from MARTE) can be allocated to memory resources. This is fundamentally necessary in order to introduce the memory mapping conception (discussed in subsection 3.2.1). Eventually, notallocated tasks can be placed onto a default processor according to subsequent transformations. Moreover, coupled with tagged resources from architecture, the task allocation allows us to identify tasks that will be kernels in OpenCL.

Deployment

Although MARTE is suitable for modeling purposes, it lacks the means to move from high level modeling specifications to execution platforms. Gaspard2 bridges this gap and introduces additional concepts and semantics to fill this requirement for System-on-Chip (SoC) co-design. Gaspard2 defines a notion of a Deployment specification level [START_REF] Rafiq | MARTE based model driven design methodology for targeting dynamically reconfigurable FPGA based SoCs[END_REF] in order to generate compilable code from an application model. This level is related to the specification of elementary components (ECs): basic building blocks of all other components having atomic functions. Although the notion of deployment is present in UML, OpenCL (and others) design has special needs, not fulfilled by this notion. In order to generate an entire system from high level specifications, all implementation details of every EC have to be determined. Low level behavioral or structural details are much better described by using usual programming languages instead of graphical UML models. Thus, IPs (Intellectual Property), very optimized and normally-parametrized functions that depend of target technology, are associated to ECs.

Transformations

In MDE, a model transformation is a compilation process which transforms a source model into a target model. The source and the target models are respectively conformed to the source and the target metamodels. A model transformation relies on a set of rules. Each rule clearly identifies concepts in the source and the target metamodels. Such decomposition makes easier the extension and the maintainability of a compilation process: new rules extend the compilation process and each rule can be modified independently from the others. The rules are specified with languages. The language may be imperative: it describes how a rule is executed; it can be declarative, it describes what is created by the rules. Declarative languages are often used in MDE because the rules objectives can be specified independently from the execution. A graphical representation is a good approach for representing the rules expressed in a declarative language.

The figure 4 illustrates an OpenCL transformation chain defined according to our model transformation engine. Two types of transformation are implemented: model to model and model to text transformation. The transformation engine is compliant with the Meta-Object Facility Query/View/Transformation (MOF QVT) [START_REF] Omg | M2M/Operational QVT Language[END_REF], proposed by OMG. Currently, in order to standardize the model transformations and to render them compatible with the future versions of the MARTE profile, we have chosen QVTO as the transformation tool for Gaspard2. The last transformation is based on Acceleo Tool [START_REF] Obeo | Acceleo -Model to Text transformation[END_REF]. Acceleo pro-

RR n°7525

vides templates that helps to transform model elements into text syntactically according to target's grammars.

Model to Model

The block number 1 in the figure 4 represents the whole model (application, architecture, deployment, and allocation). This block is an UML(according to UML+MARTE metamodel) model and is the start point. Here, we no longer use UML profile for MARTE. In order to make simple transformations and to add further concepts, we use the MARTE metamodel whose elements came from stereotypes in profile. Missed notions such as memory mapping are added to metamodel allowing to model these notions. A initial transformation converts this block into a new model conforms to MARTE metamodel. Besides, some instance concepts such as port instances (not provided by UML) are added to model in order to make distinct data among instantiated elements. The result is represented by the number 2 in the diagram.

Tilers Tilers are stereotyped in connectors between ports around the application model. The model contains connectors with the stereotype Tiler linking a part A of shape M from a port of shape N to a port of shape P of a containing component. This topology means that each element of the pattern N at the iteration M is transmitted to the element the array P according to origin, paving and fitting attributes of the Tiler following this formula: {origin + paving.i + (f itting.j mod shape)

|0 ≤ i < M |0 ≤ j < N }
The block number 3 is resulting transformation of tilers. Practically, the transformation performs a processing step on tilers and creates tasks that will be allocated onto available processors.

Local and Global Task Graph and Scheduling A local and a global task graphs are generated from the application model. Connectors between two tasks express their data dependence. When the characteristics of the parallel program, including its task execution times, task dependencies, task communications and synchronization are known a priori, scheduling can be accomplished off-line during compile-time. On the contrary, dynamic scheduling, in the absence of the initial information, is done on-the-fly according to the state of the system. Two distinct models of the parallel program have been considered extensively in the context of static scheduling: the task interaction graph (TIG) model and the task precedence graph (TPG) model [START_REF] Kwok | Static scheduling algorithms for allocating directed task graphs to multiprocessors[END_REF]. In order to choose a scheduling algorithm, we first introduce the directed acyclic graph (DAG) model, and then we propose a valid scheduling list based on data dependence order (TPG). It is important to mention that OpenCL allows to define asynchronous task scheduling from host dispatcher. Moreover, compute devices have a not-configurable internal scheduling algorithm for launched tasks. The task graphs and scheduling policy are provided from a two-transformation set highlighted with the number 4 transformation chain (fig. 4).

Memory Allocation MARTE lacks concepts that allow to describe memory allocations. We have specialized an extension for memory concepts in modeling device architecture. The main problem resides in how to set a memory space, how to define allocations to different host and devices and moreover, how to integrate all data ports (flowPorts) defined in the application model. In order to answer these questions, we have proposed a memory mapping metamodel. The next paragraphs depicts the technical details of this metamodel.

The figure 5 shows the abstract syntax that defines memory mapping concepts. Two new classes were created to add concepts for data allocation over a memory map: MemoryMap and DataAllocate. An AssemblyPart, generally an instance of memory component in the defined architecture model, should have one memoryMapping of MemoryMap type which is composed or not by dataAllocations of the DataAllocate type. Each dataAllocation has its data scopes. This scope (spaceAddress) is defined by addressSpaceQualifiers = {global, constant, local, private} such as specified in Compute Device memory hierarchy. Additionally, the dataAllocation has the following properties:

1. baseAddress: of the long integer data type and it specifies the base reference value or the base pointer of the variable;

2. dimAllocation: this information comes from flowPorts shape in the model and it defines the allocation size;

3. associatedParts: it lists all the elements in the model that use the same allocation;

4. typeAllocation: this information comes from flowPorts type in the model and it defines the variable datatype.

This metamodel, also known as MemoryMapping metamodel extension for MARTE, allows us to specify variables and their attributes. The respective transformation obtains the most of allocation details from flowPort elements which are specified in the application model. The resulting model (block 5) is part of the transformation chain in figure 4.

RR n°7525

Figure 5: Memory Mapping Metamodel

Hybrid Model The nearest metamodel to OpenCL definitions and syntax is the Hybrid metamodel that generates the Hybrid model. The figure 6 depicts the elements that help to create a real compilable application. This metamodel is strongly inspired by GPGPU (General-Purpose computation on Graphics Processing Unit) programming model. Actually, even if OpenCL defines a generic compute device in its platform model, GPU devices are well suitable to this approach.

Analysing the metamodel, we can verify that a new hierarchy of elements is added to the transformed model. The start element in this hierarchy is the Hybrid_App, the global representation of OpenCL application itself. From this point, we split the application into two parts: HostSide and DeviceSide. These parts are unique instances and they characterize tecnhically host and device roles defined by OpenCL. The HostSide and DeviceSide inherit from Execution-Side. Thus, both can instantiate Functions that represent tasks from application model. Kernels, a special function in the device side, are tasks with only one LaunchTopology. Launching a kernel requires the specification of the dimension and size of the "thread-grid". The OpenCL specification contains details about the structure of those grids. In order to define a dimension, we analyze two aspects: number of threads and data structure organization. We use a simple algorithm implemented on QVTO language to calculate the grid dimensions. The LaunchTopology element specified in the figure 6 has 3 attributes (dim, global, local ). The attribute dim is an 2-elements array containing the shape dimension of the respective kernel and total(shape internal product) of repetitions. The other attributes (global and local) are respectively the total number of WI (described in the section 2.1) and the number of WI per block or WG. With regard to respect the grid constraints (CL_DEVICE_MAX_WORK_ITEM_SIZES from clGetDeviceInfo() function, defined by OpenCL specification), the local dimension is calculated to address these limitations. Consequently, global dimension is achieved as function of total and local dimensions. Thus, a set of at least "total task repetition value" WI (work-items or threads) will be launched as illustrated in figure 7.

RR n°7525

At the scheduling level, the metamodel provides an ordered list of functions (scheduling relationship). This list is associated to each composed task (hierarchical) according to function call order. Therefore, as kernels (from device side) and main function (from host side) are composed tasks, each one has a ordered list based on previous scheduling model-to-model transformation. Another relationship, the list (functions), allows to enumerate functions hierarchically below the function itself.

The Memory Allocation model is the main source to generate variable conception in Hybrid model. Actually, characteristics such as scope, type, size, reading/writing, etc. are evident information retrieved from precedent models. However, OpenCL has other characteristics of variables besides the conventional ones. In order to cover these other characteristics, we propose two relation types between variables that help to implement the distributed aspect inherent to OpenCL memory model. The first one is refersTo relationship. This relationship allows to find which host variables should be transferred (both directions) to device variables. The second one, composed by indexin and indexout, allows to express the tiler between data elements. This information is a key aspect in order to determine which part of data an WI will process. In this case, tiler functions provide, for example, how each WI gathers or scatters data from/into global memory.

The transformation towards Hybrid model generates a model with all elements ready to create OpenCL code. It is important to note that we preserve previous information defined in previous models. Thus, main function, kernel functions, IP (elementary tasks) functions, variables (global, local, parameters), communication (data transfer) information, parallelism topology, and others are added/referenced to precedent model. The next step consists in, based on templates, to write code out.

Model to Text

If the Hybrid model was well specified, then the code generation is a trivial step made by template editors. Obeo [START_REF] Obeo | Acceleo -Model to Text transformation[END_REF] supplies the Acceleo plug-in to anyone wishing to benefit from the advantages of MDE. With Acceleo proprietary scripts (current versions have syntax elements based on the Model-to-Text OMG standard), the tool makes it possible to generate files from UML, MOF, EMF and other models. We have adopted the Acceleo solution for its suitable characteristics to MDE, such as incremental generation, debugging and the deployment of generation scripts in the form of plug-in Eclipse.

4 Case Study

Downscaler

As example to illustrate our approach, let us consider the video functionality of image digital processing system. The modeled application is an H.263 [3] video encoder. The part of the video functionality modeled here deals with scaling. It consists of a classical downscaler, which transforms a video graphics array signal (Common Intermediate Format -CIF) into a quarter video graphics array (QCIF) signal, pixels per frame. Therefore, a downscaling of 4:1 is required. Such operation is interesting when visualizing high quality live video in thinfilm transistor screen while using low power and real-time previews e.g.: view mode in video functionality of a cell phone. The downscaler itself is composed of two components: a horizontal filter that reduces the number of pixels from a 352 columns to a 176 columns frame by interpolating packets of 8 pixels; and a vertical filter that reduces the number of pixels from a 288 lines to a 144 lines frame by interpolating packets of 8 pixels as well.

Gaspard2 Model for Downscaler

In order to create an application we use the framework of Gaspard2. This framework uses the Integrated Development Environment(IDE) Eclipse [START_REF]Eclipse Modeling Framework[END_REF]. The Gaspard2 model of the downscaler application is illustrated in the figure 8. The model describes an instance of MainApplication that consists of 300 repetitive tasks Downscaler2Frame. This task is represented by two single tasks for the video reading and presentation (FrameGenerator and FrameConstructor ) and an hierarchical task consisting of three levels: top level, a repetitive task referred to as Downscaler ; second level, a compound component represented by a directed acyclic graph where the nodes are repetitive tasks HorizontalFilter and VerticalFilter ; and third level, elementary tasks HFilter and VFilter that are repeated within the repetitive tasks of second level.

Application Model Example

The whole downscaler receives frames from a 30fps CIF format 10-seconds video, denoted by the input 2D array (352,288), and produces a set of 300 transformed frames in QCIF format (176x144). The video pixels are encoded in 12-bit (a byte integer) YUV (4:2:0) color format. The FrameGenerator in each iteration(n of 300) of the Downscaler2Frame retrieves one frame of 352x288 12-bit pixels. This task split the pixels into three parts: Y for the luminance component (the brightness) and U(Cb) and V(Cr) for the chrominance (color) components. The horizontal and vertical filters have 3 repetitive tasks, one for each color/brightness section. These tasks repeat according to bytes processed at time. For example, the yhfk instance of YHFi2Block is a [288,44] repetitive task and has an input 11-bytes(8-bits integer) port. The tiler specified in this example allows to gather 11 luminance component from a 352x288 frame, the task repetition grants the whole scanning (considering the pixel interpolation) of the frame.

Architecture Model Example

The proposed host and device architectures do not explore the memory hierarchy. This simplify data allocations and communications for this Downscaler example. Thus, the architecture (figure 9) con- Allocation Model Example Subsequently, with application and architecture models defined, we can make the allocation procedure. Allocation, as showed in the section 3.1.3, implies task and data allocation. The first one indicates who executes the task. This allocation is made using an UML abstraction connector (stereotyped as allocate) that creates a link between task defined in the application model and the processor defined in the architecture model. This link will allow to identify OpenCL kernels. Default behaviors are considered in allocation step. For instance, tasks, not explicitly allocated, are executed by host processor. The figure 10 illustrates three tasks (yhfk, uhfk and vhfk ) allocated onto gp, an instance of GPU processor. Consequently, these tasks will be kernels in the Hybrid model. The application developer is the responsible to define which tasks are allocated on which compute devices. There is no explicit rule, although repetitive tasks with intensive data processing are the best candidates. The figure 11 depicts a simple example to allocate flowPorts onto memory components. Usually, these allocations follow task allocations at architecture level. Otherwise, inconsistency will occur in data access. According to Hybrid metamodel, during the code generation, transformations inquiry interconnected ports allocated onto distinct processors. Case it happens (and it should), this represents data transfers between allocated memories. This situation is illustrated in the figure 11, when the flowPort of the internal task yhfk is allocated onto gpgm, an instance of the GPU global memory, and another flowPort is allocated onto the gm, an instance of the CPU global memory.

Deployment Model Example

In design time, it is not necessary to re-write code details of the Downscaler example. Basic functions (IP) can be deployed over elementary components. These IPs are normally optimized functions (code The figure 13 shows an artifact and software IP relationship. Artifacts are a "physical" pieces of information, such as files, models, or tables. Artifacts are said to be manifested from an element abstraction. In the context of a Deployment diagram, this could be, for example, a component. This relationship is represented with the 'manifest' relationship. Among other definitions that can be set, we emphasize the source file path. The code listing 1 is just an IP example deployed on horizontal filter of the Downscaler. Transformations and Results Since we have the models defined in design time, a single step triggers the transformations illustrated in figure 4. We choose the Downscaler model (UML file) in the IDE Eclipse, then we execute the OpenCL chain. This generates source files (.cpp, .cl) and a makefile. The listing 2, it is a resulting kernel code file. Here, we discuss some generation results. For space constraints, we did not show the whole generated code, but just some key parts of the generation. At the line 3, the attribute "const" represents transformed port elements declared as "in" in the application model. The thread(WI) ID is inserted by template(line 9) and it is is automatically defined as global index in the thread grid. For this example, the rest of the code is split into 3 parts: tiler in, IP call and a tiler out. The tilers calculate the data pattern assigned to the indexed thread. The IP function processes this pattern and gives it back to another tiler (out) that writes in global memory.

[ 0 ] = ( ( a [ 0 ] + a [ 1 ] + a [ 2 ] + a [ 3 ] + a [ 4 ] + a [ 5 ] ) / 6 ) -( ( a [ 0 ] + a [ 1 ] + a [ 2 ] + ←֓ a [ 3 ] + a [ 4 ] + a [ 5 ] ) % 6 ) ; b [ 1 ] = ( ( a [ 2 ] + a [ 3 ] + a [ 4 ] + a [ 5 ] + a [ 6 ] + a [ 7 ] ) / 6 ) -( ( a [ 2 ] + a [ 3 ] + a [ 4 ] + ←֓ a [ 5 ] + a [ 6 ] + a [ 7 ] ) % 6 ) ; b [ 2 ] = ( ( a [ 5 ] + a [ 6 ] + a [ 7 ] + a [ 8 ] + a [ 9 ] + a [ 1 0 ] ) / 6 ) -( ( a [ 5 ] + a [ 6 ] + a [ 7 ] + ←֓ a [ 8 ] + a [ 9 ] + a [ 1 0 ] ) % 6
The generated code was compiled with NVIDIA's OpenCL compiler and executed in a desktop machine with a GTX285 card [START_REF] Nvidia | NVidia's Developer Zone[END_REF]. GTX285 provides 159GB/s bandwidth between its 240 cores and 1GB of GDDR3 RAM. This compares with 15-20GB/s achievable with the fastest conventional CPUs today. The result is a functional application as defined in its specifications.

RR n°7525 5 Related Work

This work is part of Gaspard2 project, essentially an MDE approach to generate code for SoC platforms. Besides OpenCL, Gaspard2 aims to generate code to other platforms such as SystemC [START_REF] Piel | Gaspard2: from marte to systemc simulation[END_REF], OpenMP [START_REF] Taillard | Openmp code generation based on an model driven engineering approach[END_REF], Synchronous [START_REF] Gamatié | Synchronous modeling and analysis of data intensive applications[END_REF], VHDL [START_REF] Rafiq Quadri | Marte based modeling approach for partial dynamic reconfigurable fpgas[END_REF] and Pthread [START_REF]Graphical array specification for parallel and distributed computing[END_REF] using respective transformation chains. These chains are designed according to intrinsic characteristics of each target platform.

Additionally, we can mention the Single Assignment C (SAC). SAC [START_REF] Scholz | Single assignment c -efficient support for high-level array operations in a functional setting[END_REF] is a strict purely functional programming language whose design is focused on the needs of numerical applications. Particular emphasis is laid on efficient support for array processing. Efficiency concerns are essentially twofold. On the one hand, efficiency in program development is to be improved by the opportunity to specify array operations on a high level of abstraction. On the other hand, efficiency in program execution, i.e. the runtime performance of programs both in time and memory consumption, is still to be achieved by sophisticated compilation schemes. Recently, it was released a branch [START_REF] Guo | Towards Compiling SAC to CUDA[END_REF] of this project that allows to generate code for CUDA. Similarities between CUDA and OpenCL were discuted in section 2.1.

In the field of OpenCL code generation, CAPS [2] proposes the CAPS HMPP toolkit. This toolkit is a set of compiler directives, tools and software runtime that supports multi-core and many-core processors parallel programming in C and Fortran. This approach is similar to a widely available standard, OpenMP, but designed to handle hardware accelerators.

Conclusions and Further Work

In this paper, we propose an MDE approach to generate OpenCL code. From an abstract model defined using UML/MARTE, we generate a compilable OpenCL code and then, a functional executable application. As MDE approach, this work intends to provide a tool for project reuse and fast development for not necessarily experts. This approach is an effective operational code generator for the newly released OpenCL standard. Further, although the case study is mono-device(one GPU) example, this approach provides resources to model applications running on multi-devices (homogeneously configured). Moreover, this work provides two main contributions for modeling with UML profile to MARTE. On the one hand, an approach to model distributed memory simple aspects, i.e. communication and memory allocations. On the other hand, an approach for modeling the platform and execution models of OpenCL.

The Hybrid metamodel proposed in this paper can be used by other target languages that conform the same memory, platform and execution models, such as CUDA language. Based on other created model-to-text templates, future works will exploit the multi-language aspect. Additionally, intelligent transformations can determine optimization levels in data communication and data access. Several studies show that these optimizations increase remarkably the application performance.

Figure 2 :

 2 Figure 2: Packages of UML Profile for MARTE

Figure 3 :

 3 Figure 3: Gaspard2 Modeling/Transformation Environment

Figure 4 :

 4 Figure 4: OpenCL Transformation Chain

Figure 6 :

 6 Figure 6: Hybrid Metamodel

Figure 7 :

 7 Figure 7: Example of Kernel Launch Grid

Figure 8 :

 8 Figure 8: Downscaler Application Model

Figure 9

 9 Figure 9: Downscaler Architecture Model

Figure 12 :

 12 Figure 12: Deployment Example

Listing 1 :

 1 IP source file example ✞ ☎ // y h f p : f i l e : h o r i z o n t a l _ f i l t e r . c l _ i n c l u d e v o i d h o r i z o n t a l _ f i l t e r ( i n t * a , i n t * b ) { b

Figure 13 :

 13 Figure 13: Software IP Association

  -compiled libraries) ready to use and available on design time. The figure12illustrates the deployment of virtualIP and softwareIP on the elementary component YVFi2Block. The deployment occurs at task and interface (data) levels. The data interface is an important deployed aspect to define parameter order, for example. Currently, multiple softwareIP, IP entry names, can be deployed on only one elementary component. Therefore, the virtualIP allows to create a interface layer in order to choose one of the available softwareIP. This feature aims to link softwareIP from different target platforms, i.e. different programming languages (Gaspard2 can generate code for multi-platforms). Nevertheless, this particularity is not present in this example.

	From application model	From architecture model
	yhfk: YHFi2Block HorizontalFilter	[288,44]	Device	Host
	uhfk: YHFi2Block	[144,22]	gpgm: GPU_GM	gm: CPU_GM
	vhfk: YHFi2Block	[144,22]
			<<abstraction>> <<allocate>>
			Figure 11: Data Allocation
	source or preYVFi2Block
	implements	implements implements
	YVFi2Block_VIP <<virtualIP>>
	implements	implements
	YVFi2Block_SIP <<softwareIP>>	implements
	vin_ip		vout_ip

RR n°7525

Listing 2: Y-Component Horizontal Filter Kernel Source File ✞ ☎

_ _ k e r n e l v o i d k y h f ( u i n t i N u m E l e m e n t s , 2 _ _ g l o b a l i n t *


Jacques Julliand
email: julliand@lifc.univ-fcomte.fr

Hassan Mountassir
email: mountass@lifc.univ-fcomte.fr

Emilie Oudot
email: oudot@lifc.univ-fcomte.fr

VeSTA: a Tool to Verify the Correct Integration of a Component in a Composite Timed System

Keywords: simulation, integration of components, timed systems, preservation of linear-time properties

Vesta is a push-button tool for checking the correct integration of a component in an environment, for component-based timed systems. By correct integration, we mean that the local properties of the component are preserved when this component is merged into an environment. This correctness is checked by means of a so-called divergencesensitive and stability-respecting timed τ -simulation, ensuring the preservation of all linear timed properties expressed in the logical formalism Mitl (Metric Interval Temporal Logic), as well as strong non-zenoness and deadlock-freedom. The development of the tool was guided by the architecture of the Open-Kronos tool. This allows, as additional feature, an easy connection of the models considered in Vesta to the Open-Caesar verification platform, and to the Open-Kronos tool.

Motivations

Model-checking is an attractive automatic verification method to ensure the correctness of models of systems. However, it is well-known that this method has difficulties to handle large-sized models, in particular when treating models involving timing constraints. Component-based modeling is a method often used to model timed systems. First, it consists in decomposing the system into a set of sub-systems, called components. Next, each component is modeled and the interactions between them are specified. The complete model is obtained by putting together all these components with respect to their interactions. With such a modeling, two kinds of properties can be checked to ensure the correctness of the model: global properties concerning the behavior of the complete model, and local properties concerning the behavior of one or some components. For both kind of properties, verification by model-checking is usually performed on the complete model, and thus can become difficult if the size of the model is too large.

We propose to use an alternative method for the verification of local properties of the components: integration of components. Integration of components is an incremental development method. It consists, for a local property L of a component C, in checking L only on C. Model-checking is here applicable due to the generally small size of the components. Obviously, L has to be preserved when C is integrated in an environment E. When using the classic parallel composition operator || between components, the preservation of local safety properties of C on C E is ensured for free. This is not the case for local liveness properties.

Simulation relations are a way to ensure preservation of properties. They have already been used in the untimed case for this purpose. For instance, [START_REF] Bellegarde | Ready-simulation is not Ready to Express a Modular Refinement Relation[END_REF] defines the refinement of transition systems as a kind of τ -simulation, which ensures the preservation of Ltl properties. In the timed case, a time-abstracting simulation is defined in [START_REF] Henzinger | Computing simulations on finite and infinite graphs[END_REF], but does not preserve timed properties. Timed simulation is defined in [START_REF] Tasiran | Verifying Abstractions of Timed Systems[END_REF], but does not consider the possible internal activity of the systems (internal activity is a main barrier for the preservation of liveness properties). A timed ready simulation is defined in [START_REF] Jensen | Scaling up Uppaal : Automatic verification of real-time systems using compositionnality and abstraction[END_REF], but does not allow to preserve liveness properties. To our knowledge, there is no simulation relation for timed systems, which handles internal activity of the systems, and also preserves liveness properties. Therefore, we defined in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF] a divergence-sensitive and stability-respecting (DS) timed τ -simulation for timed components expressed as timed automata [START_REF] Alur | A theory of timed automata[END_REF] and proved it can ensure the preservation of all linear timed properties which can be expressed in the logical formalism Mitl [START_REF] Alur | The benefits of relaxing punctuality[END_REF], thus in particular linear liveness and bounded liveness properties. Strong non-zenoness and deadlock-freedom are also preserved by the relation. That is, if C simulates C E with respect to this relation, all linear local timed properties of C are preserved on C||E.

The tool Vesta (Verification of Simulations for Timed Automata) was developed to automate the verification of the DS timed τ -simulation. More precisely, Vesta considers component-based timed systems, developed incrementally by integration of components, where each component is modeled as a timed automaton. It allows to check that local properties of a component (or group of components) of the system are preserved during its integration with other components of this system. The architecture of the tool was inspired by the one of the Open-Kronos tool [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]. Thus, as Open-Kronos, Vesta benefits of libraries which provide an efficient symbolic representation for networks of timed automata. This choice also allows to connect the models considered in Vesta to Open-Kronos, and also to the verification platform Open-Caesar [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation and Testing[END_REF].

The structure of the paper is the following. In section 2, we recall some background on timed systems, i.e., on the formalisms which are used in Vesta for the modeling of timed systems and their properties. This section also introduces the divergence-sensitive and stability-respecting timed τ -simulation, and its preservation abilities. Section 3 presents the tool Vesta: its architecture, the algorithms which are implemented and its graphical user interface. In section 4, we illustrate the interest of Vesta by using it to verify incrementally properties of a case study concerning a production cell. Section 5 presents some additional features of the tool. Finally, section 6 contains the conclusion and exhibits some future developments for Vesta.

Incremental verification of timed systems

We present here the preliminary notions that we consider concerning componentbased timed systems. First, we introduce timed automata which we use to model timed components, and the composition operator we use to assemble these components. Then, we present the simulation relation we defined for timed automata and recall previous results concerning the properties that it preserves during incremental development, and in particular, during integration of components.

Modeling timed systems

Since their introduction in [START_REF] Alur | A theory of timed automata[END_REF], timed automata are amongst the most studied models for timed systems. They are finite automata with real-valued variables called clocks, to model time elapsing.

Clock valuations and clock constraints. Let X be a set of clocks. A clock valuation over X is a mapping v : X → R + , associating to each clock in X a value in R + . We note 0 the valuation assigning the value 0 to each clock in X. Given a clock valuation v and t ∈ R + , v + t is the valuation obtained by adding t to the value of each clock in v. Given Y ⊆ X, the dimension-restricting projection of v on Y , written v Y , is the valuation over Y only containing the values in v of clocks in Y . The reset in v of the clocks in Y , written [Y := 0]v, is the valuation in which all clocks in Y are reset to zero, while the value of other clocks remains unchanged. A clock constraint over X is a set of clock valuations over X. The set C df (X) of diagonal-free clock constraints1 over X is defined by the following grammar:

g ::= x ∼ c | g ∧ g | true
where x ∈ X, c ∈ N and ∼∈ {<, ≤, =, ≥, >}. Diagonal-free clock constraints do not allow comparison between clocks such as xy ∼ c. Note that a clock constraint defines a convex X-polyhedron. We note zero the X-polyhedron defined by x∈X v(x) = 0. The dimension-restricting projection and reset operation can be directly extended to clock constraints. The backward diagonal projection of the Timed Automata. Let P rops be a set of atomic propositions. A timed automaton (TA) over Props is a tuple A = Q, q 0 , Σ, X, T, Invar, L where Q is a finite set of locations, q 0 ∈ Q is the initial location, Σ is a finite alphabet of names of actions, X is a finite set of clocks, T ⊆ Q × C df (X) × Σ × 2 X × Q is a finite set of edges, Invar is a function mapping to each location a clock constraint called its invariant and L is a labelling function mapping to each location a set of atomic propositions over Props. Each edge is a tuple e = (q, g, a, r, q ) where q and q are the source and target locations, g is a clock constraint defining the guard of the edge, a is the label of the edge and r is the set of clocks to be reset by the edge. We use the notation label(e) to denote the label a of the edge e. Examples of TA can be found in section 4. Semantics. The semantics of a TA A is an infinite graph G(A) in which states are pairs (q, v), where q is a location of A and v a clock valuation over the clocks of A, such that v ∈ Invar(q). The transitions of this graph can be either discrete or time transitions. Consider a state (q, v). Given an edge e = (q, g, a, r, q ) of A, (q, v) e → (q , v ) (where v = [r := 0]v) is a discrete transition in G(A) if v ∈ g and v ∈ Invar(q ). We call (q , v ) a discrete successor of (q, v). Time transitions have the form (q, v) t → (q, v + t) where t ∈ R + and v + t ∈ Invar(q). We say that (q, v + t) is a time successor of (q, v). Symbolic representation. Due to the dense nature of time, the semantic graph of a TA has an infinite number of states. To perform algorithmic analysis for TA, a finite representation of this state space is needed. The symbolic representation currently used is based on the notion of zones, and leads to a symbolic graph called simulation graph. A zone (q, ζ) is a set of (semantic) states of a TA, such that they have the same discrete part q and the set of their valuations forms a convex polyhedron ζ. Given a zone z = (q, ζ), we note disc(z) the discrete part q of z, and poly(z) its polyhedron ζ. The transitions of a simulation graph are labelled by discrete actions (intuitively time elapses inside zones, and thus there are no transitions labelled by time delays). The following operations allow to compute the transitions of a simulation graph: time-succ(z) and time-pred(z) represent respectively the set of time successors and predecessors of some state in z, while disc-succ(e, z) and disc-pred(e, z) represent the set of discrete successors of some state in z, by taking transition e. The operation post(e, z, c) 2 computes the successor zone of z by taking transition e, with respect to a constant c ∈ N (in general, this constant is the greater constant appearing in the constraints of the TA), while the operation pre(e, z) computes the predecessor zone of z by transition e.

X-polyhedron ζ defines a X-polyhedron ζ such that v ∈ ζ if ∃t ∈ R + • v + t ∈ ζ. The forward diagonal projection of ζ defines a X-polyhedron ζ such that v ∈ ζ if ∃t ∈ R + • v -t ∈ ζ. Given c ∈ N,
time-succ(z)

def = {s | ∃s ∈ z, t ∈ R + s t → s } time-pred(z) def = {s | ∃s ∈ z, t ∈ R + • s t → s } disc-succ(e, z) def = {s | ∃s ∈ z • s e → s } disc-pred(e, z) def = {s | ∃s ∈ z • s e → s } post(e, z, c) def = Approx c (time-succ(disc-succ(e, z)))
pre(e, z) def = disc-pred(e,time-pred(z)) 2 The operation post is used to compute the simulation graph. The use of the operator Approx c in its definition ensures the termination of the construction of the simulation graph. More details can be found in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF].

Consider a TA A = Q, q 0 , Σ, X, T, Invar, L and c ∈ N a constant greater or equal to the greatest constant appearing in a constraint of A. The simulation graph of A with respect to c, written SG(A, c), is a tuple Z, z 0 , Σ, E where Z is the finite set of states of the graph (i.e., a set of zones) and z 0 = (q 0 , zero ∩ Invar(q 0 )) is the initial zone. The set E ⊆ Z × T × Z of transitions is defined as follows: given a zone z and an edge e ∈ T , if z = post(e, z, c) = ∅, then z is a zone of the graph and z e → z is a transition of the graph.

Classic parallel composition operator for TA. We consider timed systems modeled in a compositional framework. Each component is modeled as a TA, and components are put together with some parallel composition operator. We consider here the classic parallel composition operator for TA. This operator, written , operates between TA with disjoint sets of clocks. It is defined as a synchronized product where synchronizations are done on actions with identical labels. Other actions interleave and time elapses synchronously between all the components. Formally, let us consider two TA

A i = Q i , q 0i , Σ i , X i , T i , Invar i , L i for i = 1, 2, such that X 1 ∩ X 2 = ∅. The parallel composition of A 1 and A 2 , written A 1 A 2 , creates a new TA which set of clocks is X 1 ∪ X 2 and which labels are Σ 1 ∪ Σ 2 .
The set Q of locations consists of pairs (q 1 , q 2 ) where

q 1 ∈ Q 1 and q 2 ∈ Q 2 .
The initial location is the pair (q 01 , q 02 ). The invariant of a location (q 1 , q 2 ) is Invar(q 1 )∧Invar(q 2 ), and its label is L(q 1 )∪L(q 2 ). The set T of edges is defined by the following rules: Interleaving:

(q1,q2)∈Q , (q1,g1,a,r1,q 1 ) ∈ T1 , a ∈Σ2 ((q1,q2),g1,a,r1,(q 1 ,q2)) ∈ T (q1,q2)∈Q , (q2,g2,a,r2,q 2 ) ∈ T2 , a ∈Σ1 ((q1,q2),g2,a,r2,(q1,q 2 )) ∈ T Synchronization:

(q1,q2)∈Q, (q1,g1,a,r1,q 1 ) ∈ T1 , (q2,g2,a,r2,q 2 ) ∈ T2 ((q1,q2),g1∧g2,a,r1∪r2,(q 1 ,q 2 )) ∈ T

Simulation relations to preserve properties

Recall that we are interested in developing incrementally component-based timed systems, by integration of components. The major issue when using such a method is to ensure preservation of already checked local properties of a component, when integrating it in an environment. We defined in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF] a divergencesensitive and stability-respecting (DS) timed τ -simulation, which ensures the preservation of linear timed properties, in particular safety, liveness and boundedliveness ones.

Consider a component C to be integrated in an environment E, using the parallel composition operator , where each component is modeled as a timed automaton. This integration leads to a composite automaton C E, which contains new clocks and new actions comparing to C. New clocks are the clocks of E, and new actions are internal actions of E which do not synchronize with an action of C. In C E, we consider such actions as being non-observable and rename them by τ . The DS timed τ -simulation is defined between the traces of C||E and C and is characterized by (i) if C||E can make an action of C after some amount of time, then C could also make this action after the same amount of time (clauses 1 and 2 of Definition 1), (ii) internal actions of the environment E (called τ ) stutter (clause 3 of Definition 1). Note that this definition actually corresponds to the classic notion of τ -simulation, that we extend to handle time. We also add two criteria to the definition of this simulation, namely divergence-sensitivity and stability-respect. Divergence-sensitivity ensures that internal actions τ of E will not take the control forever, and stability-respect guarantees that the integration of C in E will not create new deadlocks.

In order to avoid too many definitions, we remained concise in the presentation of the simulation and focus here directly on its symbolic formal definition, which is the one implemented in the tool Vesta. More details, as well as the definition at the semantic level, can be found in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF]. However, the following technical points used in Definition 1 must be clarified. The predicate free, used in the clause stability-respect, was defined in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]. Informally, given a location q of a timed automaton, free(q) is the set of all valuations (of states with q as discrete part) from which a discrete transition can be taken after some time elapsed. The formal definition is: free(q) = e=(q,g,a,r,q )∈T (g ∩ ([r := 0]Invar(q ))).The predicate src val, used in the clause strict simulation is defined formally as follows: src val(z, e, z ) = poly(pre(e, z ) ∩ z). It represents the valuations of the subset of states in z which lead to states in the zone z by taking transition e and letting time elapse.

Definition 1 (Symbolic DS timed τ -simulation). Let SG 1 = Z 1 , z 01 , Σ 1 , E 1 and SG 2 = Z 2 , z 02 , Σ 1 ∪ {τ }, E 2 be
two simulation graphs, obtained respectively from two TA A 1 and A 2 . The symbolic DS timed τ -simulation Z ds is the greatest binary relation included in

Z 2 × Z 1 , such that z 2 Z ds z 1 if: 1. Strict simulation: z 2 e2 → z 2 ∧ label(e 2 ) ∈ Σ 1 ⇒ ∃z 1 • (z 1 e1 → z 1 ∧ label(e 1 ) = label(e 2 ) ∧ src val(z 2 , e 2 , z 2 ) X1 ⊆ src val(z 1 , e 1 , z 1 ) ∧ z 2 Z ds z 1 ).
2. Equality of delays and of common clocks valuations: poly(z 2 ) X1 ⊆ poly(z 1 ).

τ -transitions stuttering:

z 2 e2 → z 2 ∧ label(e 2 ) = τ ⇒ z 2 Z ds z 1 .
4. Stability respect: (poly(z 2 )\free(disc(z 2 )) X1 ⊆ poly(z 1 )\free(disc(z 1 )).

5. Divergence sensitivity: SG 2 does not contain any non-zeno τ -cycles. A nonzeno τ -cycle is a cycle which only contains transitions labelled by τ and in which the total time elapsed goes to infinity (i.e., time diverges).

We extend this relation to simulation graphs. Consider two simulation graphs SG 1 and SG 2 , which initial zones are respectively z 01 and z 02 . We say that SG 1 simulates SG 2 with respect to Z ds , written SG 2 Z ds SG 1 , if z 02 Z ds z 01 .

Preservation abilities. The DS timed τ -simulation preserves all properties which can be expressed with the logic Mitl (Metric Interval Temporal Logic) [START_REF] Alur | The benefits of relaxing punctuality[END_REF], as well as strong non-zenoness and deadlock-freedom. Formal proofs can be found in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF]. Mitl is a linear timed logic, which can be viewed as the timed extension of the linear (untimed) logic Ltl [START_REF] Pnueli | The temporal logic of programs[END_REF] and in which temporal operators are constrained by a time interval. Strong non-zenoness is a specific essential property of timed systems. A TA is said to be strongly non-zeno if time can diverge along each path of its semantic graph. Note that the timed τ -simulation, without divergence-sensitivity and stability-respect criteria, preserves all safety properties.

Composability. Composability is an essential property for integration of components. Indeed, it expresses that a component automatically simulates its integration with other ones. Formally, given components C and E, it means that C simulates its integration with E, i.e., the composition C E. Thus, composability can ensure the preservation of local properties of C for free (properties preserved depends on the notion of simulation which is considered). The composability property is guaranteed with the timed τ -simulation (without divergence-sensitivity and stability-respect), when integration is achieved with the classic parallel omposition operator. This implies that safety properties are preserved for free during this integration process. However, this is not the case when considering the divergence-sensitivity and stability-respect criteria. Composability does not automatically hold. To ensure this property, the DS timed τ -simulation has to be checked algorithmically. Therefore, we implemented this verification in a tool named Vesta.

The tool Vesta

Vesta considers component-based timed models consisting of a set of components (modeled as timed automata) which interact using the classic parallel composition operator . Therefore, it provides graphical and textual editors to capture these elements. Then, Vesta can automatically generate composite systems, made up by parallel composition of chosen components with respect to the given interactions.

The main feature of Vesta is to check if local properties of a component are preserved when it is merged into an environment, by checking if this component simulates the composite system obtained by this merging. The simulation can be checked either in a "general way", i.e., to ensure preservation of all the local properties of a component, or "partially", i.e., for some specific given properties. This partial verification is presented in details in section 5.1. In both cases, if the simulation is not checked successfully, the tool reports the error found as well as a graphical diagnostic consisting of the trace of the composite system which is not simulated by any traces of the component, and the trace of the component it had to correspond to.

Architecture of Vesta

Vesta was developed using both C and Java languages. Java is used for the graphical user interface, which is described in the next section, and C for the core of the tool, which is described below. The architecture of Vesta is shown in Fig. 1. The models considered consist of three kinds of elements: the set of components (saved in .aut files) and possibly their local properties (prop) in the case of partial verification, the types of the variables used in the components and the interactions between components (sync). From this modeling, Vesta can automatically generate composite systems by using the classic parallel composition operator between the components (.exp files). Compositions can also have local properties.

To get an efficient representation of this model, Vesta is based on SMI3 (Symbolic Model Interface). SMI is a powerful library providing efficient representation for finite-state models, by building an equivalent symbolic representation using decision diagrams. Note that our choice was guided by the functioning of the Open-Kronos tool [START_REF] Tripakis | The analysis of timed systems in practice[END_REF], which is already based on SMI. The core of the tool consists of two modules: translator and simul, taking as input two components, which can be composite systems (.exp files): one corresponding to a component C to be integrated in an environment E, and the other to the composite system C||E obtained after having integrated C in E. translator creates a file .c which implements data structures and functions to generate a symbolic graph (the so-called simulation graph) for each input component. The way data structures and functions are created for C||E allows it to be connected to the different modules of Open-Caesar. When this file is created, it is compiled and linked to Open-Caesar and Dbm libraries (Dbm libraries allow to manipulate the timing constraints of the model). Then, an executable simul is created and run to check the stability-respecting timed τ -simulation. The divergence-sensitivity part is checked thanks to an adaptation of an algorithm of the module Profounder [START_REF] Tripakis | Checking Timed Büchi Automata Emptiness Efficiently[END_REF] of Open-Kronos. This algorithm, as well as the one implemented in simul, is presented in the next section.

Algorithms

The DS timed τ -simulation is checked in two phases. The divergence-sensitive part (i.e., clause 5 of Def. 1) is checked independently with an adaptation of an algorithm of the module Profounder, which is part of the Open-Kronos tool. Then, the stability-respecting timed τ -simulation is checked in the module simul (i.e., clauses 1 to 4 of Def. 1). Thus, Vesta uses two main algorithms to check the DS timed τ -simulation: one for divergence-sensitivity, and the other for the stability-respecting timed τ -simulation.

Adaptation of the module Profounder to check divergence-sensitivity.

For this verification, we use the algorithm called full DFS (full Depth First Search) defined in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF][START_REF] Tripakis | Checking Timed Büchi Automata Emptiness Efficiently[END_REF]. This algorithm was first designed to test the emptiness of a timed Büchi automaton, in the case of a persistent acceptance condition (i.e., from one point on, the automaton only visits accepting states). The algorithm thus consists in detecting non-zeno cycles in the automaton such that they only contain accepting states. For this, it visits all the paths of the simulation graph of the automaton, and puts them in a stack. The exploration of a path stops when reaching a state which is already in the stack (this means that an elementary cycle is found). It only remains to check that the cycle is non-zeno and only contains accepting states.

Algorithm 1 presents the adaptation of this algorithm to detect non-zeno τ -cycles, instead of non-zeno accepting cycles, in a simulation graph SG = Z, z 0 , Σ, E , where the alphabet Σ contains the action τ . When a cycle is detected, we test if it is non-zeno and if all the transitions of the cycle are labelled by τ . The procedures Top, Push and Pop are classic operations on stacks, allowing to get the top of a stack, and to add and remove an element in the stack. The procedure Part(Stack, e) gets all the elements of the stack Stack added after the element e. The procedure Next(Stack, e) gets the element following e in Stack (i.e. the element added after e). The procedure non zeno is defined as in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF] and performs a syntactic test to check if a path is non-zeno. This test consists in checking that, in the cycle, there exists a clock x which is reset at a point i of the cycle, and that x has a lower bound at a point j of the cycle. Intuitively, this allows to ensure that at least one time unit elapses at each loop in the cycle.

Graphical User Interface

The GUI of Vesta is shown in Fig. 2. The tree on the left is an explorer to navigate between the elements of the model, the generated assembling of components, and the results of already checked preservations (i.e., simulations). The bottom-right part is a log window, displaying informations such as syntax errors or summarized results of preservation checkings. The top-right part is the main element of the GUI, with five tabs:

-the Types tab displays the types of the variables used in the model, -the Interactions tab shows the interactions between the components, -the Basic Components tab contains all the components of the model, -the Composite Components tab contains the assembling of components, -the Simulations tab contains results for each already checked preservation. The menubar and toolbar provide buttons to treat a new model. They allow to create new components, import components from another model, choose components to put together and automatically create the assembling, and check simulations. The interactions between components can be created graphically via the Interactions tab. Components (i.e. timed automata4 ) are described through a textual editors, with a simple language which consists in giving the invariant of each location, and the transitions of the component (name, source and target location, guard, reset and, possibly, update of some variables).

Vesta in practice: incremental verification of a production cell

The tool Vesta allowed us to show the interest of incremental development by integration of components, formalized by the DS timed τ -simulation, in comparison to a direct verification on the complete model of the system. We present in this section a case study concerning a production cell 5 . This case study was developed by FZI (the Research Center for Information Technologies, in Karlsruhe) as part of the Korso project. The goal was to study the impact of the use of formal methods when treating industrial applications. Thus, this case study was treated in about thirty different formalisms. We treated it with timed automata, as it was in [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF].

Presentation of the case study The production cell contains six devices, as shown in Fig. 3: a feed-belt equipped with a sensor, a deposit-belt, an elevatingrotary table, a two-arms robot and a press. It also contains one or several pieces to be treated. Our modeling of the cell follows the one of [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF]. Description of the production cell. A simplified functioning of the cell is the following. Pieces arrive on the feed-belt. The sensor detects when a piece is introduced in the cell, and sends a message to the robot to inform that the piece is going to be available. When it arrives at the end of the belt, it is transferred to the table, which goes up and turns until being in an adequate position to give to the robot the possibility to take it. The robot turns 90 • so that its arm A can pick the piece up, and then puts it in the press which processes it. When the treatment is finished, the piece is taken by the arm B of the robot, which transports it to the deposit-belt where it is evacuated. The behavior of each device depends on timing constraints and is modeled by a timed automaton. In the sequel, we focus particularly on local properties concerning the robot, and the assembling robot press. Fig. 4 and5 show respectively the timed automata modeling the robot and the press. Some local properties. We identified seven main properties of the robot: two safety properties (called P 1 and P 2 ), two liveness (response) properties (P 3 and P 4 ) and three bounded liveness properties (P 5 , P 6 and P 7 )6 . We also identified a main liveness property (P 8 ) ensuring the correct functioning of the robot and the press when they are put together. We express these properties in Mitl7 .

¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¡ ¢ ¡¢
§ ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡ ¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡ẗ
Our objective is to compare direct verification and incremental verification by integration of components, for Mitl properties. The first method consists in assembling all the components, and then to check properties P 1 to P 8 on the complete model obtained. The second method consists in checking these properties locally only on the components they concern, and then to ensure they are preserved when these components are integrated in their environment. That is, properties P 1 to P 7 are checked on the robot component, and property P 8 on the assembling robot press. Then, the preservation of P 1 to P 7 must be ensured when the robot component is integrated with the press component. The preservation of P 8 must be guaranteed when this assembling is integrated with all the other components of the system. In this way, each locally checked property will hold on the complete model, since preservation is checked thanks to the DS timed τ -simulation, which is a preorder, and thus, is a transitive relation.

Experimental results for the production cell. First note that Vesta is not a model-checker. Thus to check the properties locally and globally, we used the model-checker Kronos [START_REF] Yovine | Kronos: A verification tool for real-time systems[END_REF]. Kronos is a verification tool for timed systems which performs Tctl model-checking [START_REF] Alur | Model-Checking in Dense Real-time[END_REF]. Tctl is a logical formalism that allows to express branching-time properties. Even if we do not consider branching-time properties, we can use it for this example since the Mitl properties we consider can also be expressed in Tctl 8 . It turns out that the local and global verification of all the properties, achieved with Kronos, succeeded. Vesta allows to ensure the preservation of locally established properties. Therefore, it is first used to check that the local properties of the robot are preserved when it is combined with the press, and then that the property of the assembling robot press is preserved when these components are integrated with the rest of the components of the cell and one piece. In both cases, the verification succeeded, and thus, the preservation of the Mitl properties P 1 to P 8 is guaranteed (as well as the preservation of strong non-zenoness and deadlock-freedom). Fig. 6 presents the results obtained on the example, by comparing incremental verification by integration of components to direct verification. We compared the time consumed to perform this direct verification on the whole model (column "Global Verification") and the time spent to achieve incremental verification, i.e., local verification and preservation checking. It turns out that, even if the computation times are still acceptable, direct verification consumes much more time (almost 20 seconds) than incremental verification when preservation is achieved with Vesta (less than one second).

Diagnostics. In section 3, we stated that Vesta has the ability to provide diagnostics when the verification of the DS timed τ -simulation (and thus of the preservation) fails. To show this functionality, we slightly modify the automaton of the press. We add a guard (for instance x p ≤ 40) to the transition plate taken by robot, which means that the press expects to be unloaded by the robot at most 40 time units after having received a piece. This modification prevents the preservation from being established, when integrating the robot with the press. Indeed, adding this guard introduces a deadlock in the assembling press robot, which did not exist in the robot component alone. Thus, deadlockfreedom is obviously not preserved. Moreover, Mitl properties P 3 to P 7 are also not preserved since non-introduction of deadlocks is precisely one of the conditions which define the DS timed τ -simulation (clause stability-respect), and thus, which ensure the preservation of Mitl properties. Note that properties P 1 and P 2 are still preserved since they are safety properties and, therefore, their preservation does not need neither stability-respect, nor divergence-sensitivity. The graphical diagnostic provided by Vesta helps detecting where the deadlock is introduced, by showing the trace of the assembling robot press where the deadlock appears, and the corresponding trace of the component robot that had to simulate it, with respect to the DS timed τ -simulation. Fig. 7 shows how diagnostics are displayed in Vesta.

Additional features

The main functionality of Vesta is to check the DS timed τ -simulation, using exactly algorithms 1 and 2. In addition, Vesta proposes an interesting additional feature, consisting in verifying partially the relation to ensure the preservation of some specific given Mitl properties. This kind of verification, as well as the motivations, are explained below.

Partial verification of the preservation

Let us go back to the second version of the production cell example, in which we modified the guard of the edge plate taken by robot in the automaton of the press. As we explained, the deadlock introduced in the assembling robot press prevents ensuring the preservation of all the properties which can be expressed for the robot, since the verification of the simulation fails. However, the specified local properties of the robot may be preserved. For this reason, we improved Vesta by giving the possibility to the user to specify the properties to preserve, and to check the preservation only for these properties (instead of a "global preservation"). This is what we call partial verification of the preservation.

Thus, the objective of such a verification is to guarantee the preservation of specified local properties of a component, rather than the preservation of all the properties which could be potentially specified. Until now, this functionality is only available for response properties of the form (p ⇒ ♦q). The reasoning for this kind of verification is the following. In most cases, the verification of the simulation fails due to an introduction of deadlocks (i.e., the clause stability-respect of the simulation does not hold). Consider now a component C, a local property L = (p ⇒ ♦q) of C and an environment E in which C must be integrated. A path π in C E, in which a deadlock is introduced comparing to the path of C which simulates it, makes the verification of the preservation fail. However, if this path π does not concern L, then the preservation should be guaranteed.

Let us detail how this partial verification is achieved, for a response property of the form (p ⇒ ♦q). To ensure the preservation of such a property, we must guarantee that, when p is encountered in a path π, this path is not cut (by the introduction of a deadlock) before q is reached. Thus, the partial verification consists in checking this non-introduction of deadlock (i.e., the clause stabilityrespect) only for the states of π located between the state satisfying p, and the one satisfying q. Fig. 8 illustrates the principle of this verification for this kind of property. A path is represented, and the states on which stability-respect must be checked are put in grey. Note also that divergence-sensitivity must also be checked for these states, to ensure that the path is not cut by means of the introduction of an infinite sequence of non-observable actions. The verification for divergence-sensitivity consists in checking that these states are not part of a non-zeno cycle only containing non-observable actions. Thus, Vesta gives the possibility to specify the local properties of C, of the form (p ⇒ ♦q), which must be preserved, and to verify the simulation only to guarantee the preservation of these properties. Note that, contrary to the classic verification, this partial verification does not guarantee the preservation of strong non-zenoness and deadlock-freedom.

Connection to other platforms and tools

Another interesting point of Vesta is the following. Recall that the way the tool was designed was inspired by the Open-Kronos tool. In particular, the syntax used to describe the components, and the symbolic representation of these models, is identical to the one in Open-Kronos. Thus, a direct consequence of this design choice is that models considered in Vesta can be connected to the Open-Kronos tool. Connection to the Open-Caesar verification platform is also possible as another direct consequence, since this connection was already available from Open-Kronos models.

The connection to Open-Kronos is particularly interesting. Indeed, the ability to connect Vesta models to Open-Kronos could allow to check Mitl properties directly on the models considered in Vesta. Recall that, now, we use the tool Kronos to perform model-checking, since there exist no tools for Mitl model-checking. Thus, as Kronos is a Tctl model-checker, we are restricted to Mitl properties which can also be expressed in Tctl. Moreover, Vesta models must be translated into Kronos syntax. The Open-Kronos tool can perform reachability analysis, but can also test timed Büchi automata (TBA) emptiness. Mitl properties can be translated into TBA which recognize the same language. Thus, with a translator from Mitl to TBA (such translators do not exist yet) and an implementation of the composition of TA with TBA (see [START_REF] Tripakis | The analysis of timed systems in practice[END_REF] to get more details about this special composition), it would be possible to directly connect Vesta models of components to Open-Kronos, perform Mitl modelchecking on these components, and then check with Vesta the preservation of these properties during the integration of these components.

  the extrapolation of ζ w.r.t. c, written Approx c (ζ), is the smallest polyhedron ζ ⊇ ζ defined intuitively as follows: lower bounds of ζ greater than c are replaced by c, and upper bounds greater than c are ignored. All these operations preserve convexity.

Fig. 1 .

 1 Fig. 1. Structure of Vesta

Fig. 2 .

 2 Fig. 2. Graphical User Interface of Vesta

Fig. 3 .

 3 Fig. 3. The Production Cell Example

  at

Fig. 4 .Fig. 5 .

 45 Fig. 4. Timed Automaton of the robot

Fig. 7 .

 7 Fig. 7. Diagnostic provided by Vesta

Fig. 8 .

 8 Fig. 8. Partial verification for a property of the form (p ⇒ ♦q)

  ¡¢ ¡¢ ¡¢ ¡¢ ¡¢ ¢ ¡¢ ¡¢ ¡¢ ¡¢ ¡¢ ¡¢ £ ¡£ ¡£ ¡£ ¡£ ¡£ ¡£ ¡£ £ ¡£ ¡£ ¡£ ¡£ ¡£ ¡£ ¡£ ¤ ¡¤ ¡¤ ¡¤ ¡¤ ¡¤ ¡¤ ¤ ¡¤ ¡¤ ¡¤ ¡¤ ¡¤ ¡¤ ¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦

table wait table

 wait

		to press
		xR = 5,
	table to robot,
	read		turn 90
	to table2
		at press2	wait2
			at press3
	at dep belt	wait dep belt	to dep belt

We restrict ourselves to this kind of clocks constraints to ensure the correctness of the construction of the symbolic representation of TA[START_REF] Bouyer | Untameable Timed Automata ! In[END_REF].

http://www-verimag.imag.fr/∼async/SMI/index.shtml

Actually, Vesta considers extended timed automata, which can be equiped with boolean, bounded-integer and enumerative-type variables. However, the use of these variables is restricted to a local use for the components (no shared variables).

The detailed results for this case study, as well as other experimentations, can be found in[START_REF] Bellegarde | Experiments in the use of τ -simulations for the components-verification of real-time systems[END_REF].

Under some conditions, safety properties express that something bad will not happen, liveness ones that something expected will eventually happen and bounded liveness ones that something expected will eventually happen within some bounded delay.

The detailed expressions of these properties can be found in[START_REF] Bellegarde | Experiments in the use of τ -simulations for the components-verification of real-time systems[END_REF].

Acknowledgments. We would like to thank Stavros Tripakis for having sent to us the distribution of Open-Kronos, particularly the module Profounder and some (useful !) source files. Thanks also for the time spent answering questions.

This work has been partially funded by the ANR-06-SETI-017 TACOS project (Trustworthy Assembling of Components: from requirements to specification). Vesta is available at the following url: http://lifc.univ-fcomte.fr/∼oudot/VeSTA.

Note that a classic DFS is generally not sufficient to detect non-zeno τcycles. Indeed, this search can miss cycles. For instance, consider a simulation graph with four states (and, to simplify only τ -transitions), such that there is a zeno τ -cycle visiting the following states: 1 → 2 → 3 → 1, and a non-zeno one 1 → 4 → 2 → 3 → 1. A simple DFS would explore the path 1 → 2 → 3 → 1 and find this zeno cycle, which is not retained for divergence-sensitivity checking. Then, the search would explore the path 1 → 4 → 2, and stop since the state 2 has already been visited. Thus, the non-zeno cycle is missed. The full DFS would not have missed this cycle since it explores all cycles. However, the drawback of this algorithm is its worst-case complexity: exponential in the size of the simulation graph [START_REF] Tripakis | Checking Timed Büchi Automata Emptiness Efficiently[END_REF]. The problem exposed above with a simple DFS comes from zeno cycles. For strongly non-zeno simulation graphs (i.e., which do not contain any zeno path), a simple DFS (linear in the size of the graph) is sufficient.

Checking the stability-respecting timed τ -simulation in the module simul. Algorithm 2 checks the symbolic stability-respecting timed τ -simulation between two simulation graphs SG 1 = Z 1 , z 01 , Σ 1 , E 1 , with set of clocks X 1 , and

The algorithm is cut in four parts, the main one being verification Z ds . A procedure verif Z and stability respect performs a joint depth-first search of SG 2 and SG 1 , and at each step of the search, it checks clauses 1 to 4 of Def. 1. A set Visited records the already visited pairs of zones in relation, and a stack Stack contains the currently checked pairs of zones. This stack also allows to return diagnostics when the verification fails.

Conclusion and further developments

In this paper, we presented the tool Vesta, which allows (i) to model incrementally a component-based timed system, by integration of components, and (ii) to ensure the preservation of established local properties of the components on the complete model, instead of performing a direct verification of these properties on this complete model. Timed components are modeled as timed automata, and integration is achieved thanks to the classic parallel composition operator for timed automata. Preservation is checked by means of a divergence-sensitive and stability-respecting timed τ -simulation. Precisely, a successful verification of this relation ensures the preservation of all linear timed properties expressed with the logic Mitl, strong non-zenoness and deadlock-freedom.

The first results obtained for incremental verification by integration of components, using Vesta for the preservation part, are encouraging. On the production cell case study of [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF], it turns out that a direct verification consumes almost 20 seconds of computation time, while the incremental one based on preservation needs less than one second. Other experiments showed that Vesta can handle models up to 400000 symbolic states. Beyond this number, we had not enough memory for the verification of the preservation to be run to completion (on a PC with 1Gb memory). Nevertheless, this number has to be relativized with respect to the number of clocks of the model, which is a direct cause of great memory consumption: 15 clocks for the model from which we obtained this upper bound. Thus, further improvements will be dedicated to handle this limitation, by implementing abstractions such as the active-clock reduction [START_REF] Daws | Reducing the number of clock variables in timed automata[END_REF][START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF], allowing to ignore clocks in states where they are inactive.

Another further development concerns the partial verification of the DS timed τ -simulation. The objective of such a verification is to check preservation only for the local properties which are specified for the components, instead of ensuring the preservation of all properties which could potentially be expressed. Until now, this partial verification is only available for response properties of the form (p ⇒ ♦q). It seems interesting to extend this kind of verification to other patterns of liveness and bounded-liveness properties. Moreover, this kind of verification could optimize computation times. Indeed, recall that partial verification consists, in particular, in checking the stability-respecting part of the simulation only on some specific states, instead of checking it systematically. As stability-respect is checked by means of high-cost operations, such as polyhedra complementation, it is essential to avoid as much as possible to check this clause. Thus, generalizing partial verification could lead to better performances in terms of computation times to check preservation.

Additional Informations. More informations on Vesta can be found in its complete documentation and user guide at the following url: http://lifc.univ-fcomte.fr/publis/papers/pub/2006/RT2006-01.pdf.