Francisco Coito
email: francisco.coito@sapo.pt

António Eleutério
email: a.eleuterio@campus.fct.unl.pt

Stanimir Valtchev

Fernando Coito

Tracking a Mobile Robot Position Using Vision and Inertial Sensor

Keywords: Mobile robotics, multi-rate sampling, sensor fusion, vision, inertial sensor

Wheeled mobile robots are still the first choice when it comes to industrial or domotic applications. The robot's navigation system aims to reliably determine the robot's position, velocity and orientation and provide it to control and trajectory guidance modules. The most frequently used sensors are inertial measurement units (IMU) combined with an absolute position sensing mechanism. The dead reckoning approach using IMU suffers from integration drift due to noise and bias. To overcome this limitation we propose the use of the inertial system in combination with mechanical odometers and a vision based system. These two sensor complement each other as the vision sensor is accurate at low-velocities but requires long computation time, while the inertial sensor is able to track fast movements but suffers from drift. The information from the sensors is integrated through a multi-rate fusion scheme. Each of the sensor systems is assumed to have it's own independent sampling rate, which may be time-varying. Data fusion is performed by a multi-rate Kalman filter. The paper describes the inertial and vision navigation systems, and the data fusion algorithm. Simulation and experimental results are presented.

Introduction

The number of industrial mobile robots applications has increased significantly in the last decades and its use in other indoor environments also shows a growing interest. Due to its simple mechanical structure and agility wheeled robots are still the first choice when it comes to industrial or domotic applications. Knowing exactly where a mobile entity is and monitoring its trajectory in real-time is an essential feature. Most applications, however, still rely on a more or less complex infrastructure to fulfill this task and that reduces the robot's autonomy [START_REF] Kim | Dynamic Ultrasonic Hybrid Localization System for Indoor Mobile Robots[END_REF][START_REF] Lee | Position Estimation for Mobile Robot Using In-plane 3-Axis IMU and Active Beacon[END_REF][START_REF] Tennina | Entity Localization and Tracking: A Sensor Fusion-based Mechanism in WSNs[END_REF].

The guidance system for a mobile robot is usually composed by three modules: trajectory generation and supervision system, control system and navigation system. The navigation system aims to determine reliable information on the robot's position, velocity and orientation and provide it to the other modules. Knowing the location of an autonomous mobile equipment and monitoring its trajectory in real-time is still a challenging problem that requires the combined use of a number of different sensors. The most frequently used sensors are inertial measurement units (IMU) [START_REF] Kim | Dynamic Ultrasonic Hybrid Localization System for Indoor Mobile Robots[END_REF][START_REF] Lee | Position Estimation for Mobile Robot Using In-plane 3-Axis IMU and Active Beacon[END_REF][START_REF] Tennina | Entity Localization and Tracking: A Sensor Fusion-based Mechanism in WSNs[END_REF][START_REF] Armesto | Multi-rate fusion with vision and inertial sensors[END_REF][START_REF] Bancroft | Data Fusion Algorithms for Multiple Inertial Measurement Units[END_REF][START_REF] Hol | Robust real-time tracking by fusing measurements from inertial and vision sensors[END_REF][START_REF] Cho | A dead reckoning localization system for mobile robots using inertial sensors and wheel revolution encoding[END_REF][START_REF] Marín | Multi Sensor Fusion Framework for Indoor-Outdoor Localization of Limited Resource Mobile Robots[END_REF]. With inertial sensors the robot's position and velocity can be computed by integrating the acceleration measurements given by the sensors, but the position and the orientation errors grow over time as a result from the accumulation of the measurements' noise and bias. As the computation position from acceleration requires two integration steps, the position error grows much faster than the error of orientation, which requires only one integration step. Thus, when an IMU is used for potion measurement it is usually combined with another position measurement system with lesser drifting error.

To tackle with this task a number of solutions are proposed in the literature. Some authors use multiple IMUs or combine them with electromechanical odometers [START_REF] Lee | Position Estimation for Mobile Robot Using In-plane 3-Axis IMU and Active Beacon[END_REF][START_REF] Cho | A dead reckoning localization system for mobile robots using inertial sensors and wheel revolution encoding[END_REF]. As all the sensors are prone to drift errors the problem is not eliminated but the precision is improved. The use of GPS as an absolute positioning system is also proposed [START_REF] Bancroft | Data Fusion Algorithms for Multiple Inertial Measurement Units[END_REF][START_REF] Marín | Multi Sensor Fusion Framework for Indoor-Outdoor Localization of Limited Resource Mobile Robots[END_REF], however this is not an option for indoor operation. A number of solutions for indoor applications use active beacons as a means to determine the absolute position of the robot [START_REF] Kim | Dynamic Ultrasonic Hybrid Localization System for Indoor Mobile Robots[END_REF][START_REF] Lee | Position Estimation for Mobile Robot Using In-plane 3-Axis IMU and Active Beacon[END_REF][START_REF] Tennina | Entity Localization and Tracking: A Sensor Fusion-based Mechanism in WSNs[END_REF]. This type of approach requires the existence of a fixed infrastructure that involves additional cost and reduces the robot's autonomy.

The Proposed System

In this work we propose the use a vision based system in combination with the inertial system to determine the robots position and velocity. The use of vision together with inertial sensors has been used by other authors [START_REF] Armesto | Multi-rate fusion with vision and inertial sensors[END_REF][START_REF] Hol | Robust real-time tracking by fusing measurements from inertial and vision sensors[END_REF]. Most systems consider the use of one or more cameras with known positions on the robot's environment. An IMU attached to a moving camera is proposed in [START_REF] Hol | Robust real-time tracking by fusing measurements from inertial and vision sensors[END_REF] to determine the grip position of an industrial robotic manipulator. Experimental results also make use of measurements from mechanical odometers included on the robot traction system.

Multi-rate Sensor Fusion

When fusing the information from multiple sensor systems each senor presents a different time delay. While inertial systems are fast, allowing sample rates in the order of several kHz at least, when vision algorithms are involved the computation time associated with feature evaluation and coordinate computation causes a significantly larger time delay. As a result the vision system position estimates are delayed, both to the robot real position, as well as to the IMU's information.

In summary, while inertial measurements are frequent and accurate on the short term, but present drift, vision information has long (variable) time delays, which renders them inappropriate for driving control purposes. Thus, the two systems are complementary to each other and the fusion of their information can improve the system overall performance.

The integration of the IMU and vision systems is done by meas of a Kalman filter (KF). As the KF is not computationally intensive, it is easily applied in real-time applications such as inertial navigation systems.

Contribution to Collective Awareness Systems

The impact information technology on every day's life is enormous and has jumped from plants to offices and the household. Most equipment embeds one or more computers and the ability to access and use web based information is increasing daily. However, the equipment ability to integrate the human environment is still limited by their lack of mobility. Households are unstructured environments and, in spite the progress in the mobile robotics area, this is still a challenge for the autonomy of mobile equipment and the ability to move around freely without supervision.

Position Estimation

In this work a wheeled robot is considered, moving on an almost plane horizontal surface, located indoors.

The Inertial Measurement System

The mobile robot dynamics is represented in two coordinate frames: the robot frame and the world frame. The robot frame is fixed onto the moving robot, usually with the origin at the center of mass, which is assumed to lie between the wheels. The world frame is fixed on the field. Fig. 1 illustrates how the two frames are related.

The IMU sensor is placed at the center of the robot. The gyroscope is aligned with the vertical axis. The position of the robot is given by: Where <x, y> is the robot position on the world frame; <v L , v T > are the longitudinal and transversal robot speed on it's own frame and θ is the orientation. The values for θ v L and v T result from the integration of the measured rotation rate and translational accelerations. In order to minimize the error these integral values are computed through a KF.

& x & y         = cos θ(t) ( ) sin θ(t) ( ) -sin θ (t) ( ) cos θ(t) ( )         v L v T         , (1)

The Vision System

The vision based odometry system uses the FAST corners method [START_REF] Rosten | Faster and Better: A Machine Learning Approach to Corner Detection[END_REF] to extract features from each image. Two consecutive images are compared and their features are matched. From this comparison the camera displacement is computed through a kinematic transformation of a frame onto the next.

The FAST corner features are referred to as corners. Each corner corresponds to a central pixel location that, on its surrounding circle of pixels (with a certain diameter), contains an arc of N or more contiguous pixels that are all much brighter than the central pixel. A corner is also found if the all the pixels on the arc are much darker than the center. Each corner on a frame is characterized by a set of features such as coordinates, pixel arc size, the arc average color and corner color.

In order to find a match between two corners from different images, all the corners in both images are compared. The comparison takes into account all the above features, as well as each corner signature. The signature of a corner in an image is the set of distances between that corner and every other corner in the same image. This feature is computationally burdensome, but the probability of two corners having a similar signature is small.

In the comparison each feature is weighted by the reverse of the frequency of occurrence. Hence, the features that are less probable to occur in different corners are given a higher relevance for corner comparison. When the same corner is found in two different images it is said to be a matching. Two matching (two points) allows the definition of corresponding coordinate frames in each of the images.

Experimental results are presented in Fig. 2. The displacement of the coordinate frame between the two images allows computing the camera movement. To increase the precision the frame displacement is computed as an average from several matching. By calculating the motion of the robot between frames, a track of the motion can be drawn. Fig. 3 represents schematically the vision system geometry. As proposed by [START_REF] Lucas | Mosaic based flexible navigation for AGVs[END_REF] the camera is located on top of the robot directed to the ceiling. It is aligned with the middle of the wheel axis line (where the IMU is also located). A known limitation stems from the fact that the pixel displacement depends not only on the robot movement, but also on the distance to the ceiling (D). As seen in the figure, there is a linear relation between the distance D (from the robot to the ceiling) and the camera generic field of view A. Hence, it is possible to calculate A by knowing D.

At present it is assumed that this value is known in advance. In the future the camera will be integrated with a distance sensor. Precision is also affected if the camera angle is not precisely perpendicular to the ceiling. This is not a limitation as the robot is aimed to work on a horizontal surface. The use of a 3-axis accelerometergyroscope IMU allows the detection of strong disturbances and the correction of constant displacement angles.

In order to minimize error accumulation, the first image of the set used to measure the robot's movement is kept as long as the number of matchings is large enough to ensure precision. Only when that fails to happen a new initial image is selected.

Multi-Rate Sensor Fusion

The two sensor systems present very different sampling rates. The vision system's sampling period is long and changes randomly. Due to its computation time the position measurements are time delayed. The proposed fusion scheme uses a discrete multi-rate KF [START_REF] Armesto | Multi-rate fusion with vision and inertial sensors[END_REF] designed to tackle with these characteristics. The state estimation is based on a discrete-time state-space description of the system dynamics:

Z k+1 = A k Z k + G k n k Y k = C k Z k + w k , (2)
where Z=[v x x v y y θ] T is the system state; Y k is the vector of measured values at time k; n k and w k are considered to be noise. The time varying matrices are:

A k = 1 0 0 0 0 ∆t k 1 0 0 0 0 0 1 0 0 0 0 ∆t k 1 0 0 0 0 0 0                 G k = 1 0 0 0 0 0 0 1 0 0 0 0 0 0 1                 , (3)
The sampling period ∆t k is the interval between consecutive data fusion moments, and may not be constant. As in [START_REF] Armesto | Multi-rate fusion with vision and inertial sensors[END_REF], at each fusion moment the set of available measured signals depends on their own sampling rates, therefore the output equations may vary because only available measurements are considered. To use the position data provided by the vision system it is necessary to take into account the computation delay. As proposed by [START_REF] Hu | Estimation Fusion with General Asynchronous Multi-Rate Sensors[END_REF], model ( 2) is used to embed the time delay of the vision measurements in the multi-rate KF.

Results

Simulation Results

The simulation results presented in this section consider the inertial system's sampling rate to be 100 Hz (average), with a sampling time uniformly distributed in the range from 9-11 milisecond. Inertial data samples are synchronous with the fusion moments. The vision system is simulated through a block that provides 2 position measurements per second, with a variable time delay on the range 0.38-0.42 second. Vision measurements are uniformly distributed within 5 cm of the true position. The noise and bias of the IMU's measurements are larger than the upper values taken from the manufacturer datasheet. For simulation purposes image position information is assumed to lie within ±3cm from the real position. The robots initial position and orientation are assumed as the origin of the real world coordinate frame. The trajectory is performed at a constant linear speed of 0.04 m/s. Different rotation rates are used along the test. Fig. 4 presents the simulated results. The robot's trajectory is tracked without significant bias. If there is any bias it does not increase with time. The position error is under 3 cm over most of the test (see Fig. 5). The deviation of the position measurement increases only when the robot performs a fast turn, with a small radius. The error is strongly affected by the vision system sample rate and delay. A faster vision system leads to smaller errors.

Experimental Results

The mobile robot from Fig. 1 is used to develop the position measurement system.

The measurement unit couples an inertial sensor (IMU) and upward directed camera positioned on top of the IMU. Both sensors are vertically aligned. The robot has two mechanically connected wheels on each side. The measurement of the wheel speed for both sides of the robot is available. The robot is coupled with a device to graphically mark the performed path. At the present stage the robot's absolute position is determined only when it stops at a still position. In Fig. 6 are presented experimental results obtained with the position measurement system. The robot performs a trajectory with four sections. Within each section the robot moves with a linear speed of 10 cm/s and turns with an angular speed of 0.2 rad/s (approx.). At the end of a section the robot stops and absolute position is determined. A Kalman filter is used to estimate the robot's position (x, y) and heading (θ) from the IMU and wheel speed measurements. The estimates are computed every 25 ms. Absolute position measurements are also included in the estimation process when they are available. The time gap between these measures is of 40 s (approx.).

Conclusions

The paper addresses the problem of measuring the position and speed of an autonomous mobile robot for indoor applications. In order to enhance the robot autonomy it is assumed that the position measurements do not require an external infrastructure. Simulation results show that proposed solution is presents a viable way to determine the robot position. The precision and sample rate adequate for most control applications.

Fig. 1 .

 1 Fig. 1. Left: Mobile robot. Right: Coordinate frames: <x, y> world frame; <L, T> robot frame; θ orientation.

Fig. 2 .

 2 Fig. 2. An example of corner detection and matching -Left: Sequence of two images taken from a ceiling. All FAST corners feature points are marked as white points. Those in the middle of white circumferences are chosen for matching between frames, and black lines point out corner matching pairs. Right: Mapping of the robot motion.

Fig. 3 .

 3 Fig. 3. Vision system image acquisition geometry. C: camera; D: distance from the target (ceiling); d: robot displacement.

Fig. 4 .

 4 Fig. 4. Simulation results: Robot position vs. measured position. Left: Robot movement and measured position. Right: x and y measurements and true values.

Fig. 5 .

 5 Fig. 5. Simulation results: Position error (in meters).

Fig. 6 .

 6 Fig. 6. Experimental results -Left: Raw measurement data. Right: x, y and θ estimation and actual values; vertical lines indicate when absolute position measurement are obtained.

Fig. 7 .

 7 Fig. 7. Experimental results -Line: Robot position. Dot: position estimate. Cross: Absolute position measurement. Circle: Initial position.


João F P Fernandes
email: joao.f.p.fernandes@ist.utl.pt

P J Costa Branco
email: 2pbranco@ist.utl.pt

A Shell-Like Induction Electrical Machine

Keywords: Electromechanic energy conversion, Electric machines, spherical induction motors, assistive devices

This paper proposes to recover the concept of spherical induction electrical machines to conceive a shell-like actuator with multi-DOF (Degrees-Of-Freedom). The actuator is formed by a shell stator and a spherical rotor. This work contains the feasibility study of that solution when applied as an active joint actuator in assistive devices. Its electromechanical characteristics are first analyzed using an analytic model that includes: the distribution of the magnetic potential vector and thus the components of the magnetic flux density in the airgap due to a sinusoidal current distribution imposed in the stator; the model also shows the induced electromotive forces and associated current density distribution in the rotor; and at last the radial and tangential components of the force density in the rotor. The shell-like actuator is concretized as an active joint for assisting movement of the lower leg of a typical 70kg person. Based on its requirements, the joint actuator electromechanical characteristics are analyzed according to its sensitivity to a set of electrical and mechanical variables.

Introduction

Nowadays, multi-DOF motion devices have been mostly formed by a composition of classic electric motors. While today multi-DOF manipulators provide enough accurate motion, the type and number of joints used means a heavy, bulky and expensive structure. Particularly in the area of assistive devices, as active joints [START_REF] Ninhuijs | Feasibility Study of a Spherical Actuator in an Arm Support[END_REF], and in some industrial applications [START_REF] Suzuki | Wafer inspection equipment and system[END_REF][START_REF] Lee | Concept Development and Design of a Spherical Wheel Motor (SWM)[END_REF][START_REF] Kawano | Pre-loading Mechanism and Angular Positioning Control Algorithm for Multi-DOF Ultrasonic Motor with a Weight Load[END_REF], these manipulators have to be compact, light, with a simple structure and also competitive cost.

This research recovers the concept of classic induction machines to conceive an innovative shell-like spherical actuator which allows multi-DOF motion while reducing the complexity of the solution. This work model and analyses its electromechanical characteristics and feasibility as a multi-DOF actuator to operate as an active joint assisting the movement of the lower leg of a typical 70kg person. The key characteristics to be analyzed due to demanded requirements are the amplitude and range of the density forces induced in the rotor and the range of its angular speed.

The paper is divided in the following three steps: the concept where the design is explained; the analytical model with the statement of its assumptions and computation of its electromechanical characteristics; and in the end the assistive device application feasibility and comparison of the analytical and its finite element simulation.

Contribution to Collective Awareness Systems

Although the main focus application is in assistive devices, i.e., in biomedical engineering systems, its applications can be easily extended to robotics and integrated manufacturing systems [START_REF] Suzuki | Wafer inspection equipment and system[END_REF][START_REF] Lee | Concept Development and Design of a Spherical Wheel Motor (SWM)[END_REF][START_REF] Kawano | Pre-loading Mechanism and Angular Positioning Control Algorithm for Multi-DOF Ultrasonic Motor with a Weight Load[END_REF] due to its 3DOF and compact solution, and also used to electric motion devices, as an active wheel [START_REF] Kagawa | Absorption of hydrogen by Vanadium-rich V-Ti-Based Alloys[END_REF].

In industrial and motion applications where 3DOF are required, this solution presents a simple control due to its reduced complexity, contributing to the simplification of the control and decision, electronics and signal processing systems.

The Concept of a Shell-Like Induction Electrical Machine

The shell-like design is inspired on the main joints of the human body as shown in Section 1. The stator acts like a socket where the spherical rotor fits, with its periphery defining the range of motion. Figures 2 and3 illustrated the concept behind the shell-like actuator as result of a high range and medium range joints.

The machine uses the same concept of classic induction motors to produce an electromagnetic torque between rotor and stator parts. Figure 4 indicates that the stator is formed by an outer ferromagnetic material layer and an inner layer composed by a distribution set of slotless coils. These will create a travelling magnetic flux density wave that will be commanded to generate an electromagnetic torque in any 3D direction.

The rotor has two layers: the outer one using an electric conductive material and an inner layer of a high magnetic permeability material.

Analytical Model

Figure 5 shows a schematic for the analytical model, which was formulated under the following assumptions: one single homogeneous zone (airgap); a thin current density layer defined as the inner stator surface; a thin electric conducting material layer (ߪelectrical conductivity) defined as the outer surface of the rotor; a high permeability ferromagnetic material on the stator and also in the rotor; and negligence of border effects due to the small size of the airgap in relation to the stator length.

To produce an electromagnetic torque it is needed the presence of a travelling wave of electromotive force (EMF) in the rotor. This will be originated by the airgap travelling magnetic wave due to the current density circulating in the stator. The EMF wave is an image of the stator current density being expressed by [START_REF] Ninhuijs | Feasibility Study of a Spherical Actuator in an Arm Support[END_REF], where k is the wavelength of the stator's EMF (equivalent to the number of poles of the stator):

ܬ Ԧ ௦ ൌ ܴ݁൛ܬ ݁ ሺఠ௧ିఝሻ ݑ ሬԦ ఏ ൟ (1)
As result the airgap potential vector will be similar to the current density. The following generic equation defines the potential vector as the composition of two components: a radial dependent component ܣሺݎሻ and a time/space dependent component ݁ ሺఠ௧ିఝሻ :

ܣ Ԧ ௭ ൌ ܣሺݎሻ݁ ሺఠ௧ିఝሻ ݑ ሬԦ ఏ ሺ2ሻ
This problem simplifies into the laplacian solution of the radial component ܣሺݎሻ. Although initially using spherical coordinates, this shell-like design will allow us to change to cylindrical coordinates, simplifying the laplacian solution computation of (2). The following figure illustrates the uniqueness of symmetry around axis -y that allows the change of coordinates. Therefore the laplacian of potential vector in cylindrical coordinates is defined by:

 ଶ ܣ Ԧ ఏ ൌ ቆ ߲ ଶ ܣሺݎሻ ݎ߲ ଶ 1 ݎ ଶ ߲ ଶ ܣሺݎሻ ߲߮ ଶ ߲ ଶ ܣሺݎሻ ߲ߠ ଶ 1 ݎ ߲ܣሺݎሻ ݎ߲ ቇ ݑ ሬԦ ఏ ൌ 0 (3)
Solution of ( 3) is the typical Cauchy-Euler solution as in (4):

ܣ Ԧ ఏ ൌ ሺܥ ଵ ݎ ܥ ଶ ݎ ି ሻ݁ ሺఠ௧ିఝሻ ݑ ఏ ሬሬሬሬԦ (4)
Constants ܥ ଵ and ܥ ଶ in (4) must be defined by two boundary problem conditions. Using the integral form of Ampere's Law, it is possible to establish the relation between magnetic flux density components and density currents on the stator and rotor. These boundary conditions are defined by equations a and b in (5), and illustrated in Fig. 7

ܽሻ න ܪ

ௗ ݈݀ ൌ න ܬ ௌ ݊ ሬԦ݀߮ , ܾሻ න ܪ ఝ ݀߮ ൌ න ܬ ݊ ሬԦ݀߮ (5)
The stator current density ܬ Ԧ ௦ is the source for the rotor EMF, resulting in the rotor induced density current ܬ Ԧ , given by (6), taking in account the electric field ܧ ሬԦ and the linear tangential velocity of the rotor, ܸ ሬԦ .

ܬ Ԧ ൌ ߪ൫ܧ ሬԦ ܸ ሬԦ × ܤ ሬԦ ൯ ൌ ߪ ቆ- ܣ߲ Ԧ ఏ ݐ߲ -߱ ܣ߲ Ԧ ఏ ߲߮ ቇ (6)
Defining the slip parameter ൌ ሺ࣓ -࣓ ሻ, constants and become given by ( 7) and (8). Term is the radius of the rotor, is the radius of the stator.

ܥ ଵ ൌ ܬ ߤ ݎ ௦ ାଵ ݇ ቀ1 ݆ ߤ ߪܵ ݇ ݎ ቁ ቆ-ݎ ଶ ݎ ௦ ଶ ݆ ߤ ߪܵ ݇ ሺݎ ଶ ݎ ௦ ଶ ሻቇ (7) ܥ ଶ ൌ ܬ ߤ ݎ ௦ ାଵ ݎ ଶ ݇ ቀ1 -݆ ߤ ߪܵ ݇ ݎ ቁ ቆ-ݎ ଶ ݎ ௦ ଶ ݆ ߤ ߪܵ ݇ ሺݎ ଶ ݎ ௦ ଶ ሻቇ (8)

Electromechanical Characteristics

The magnetic flux density is given by the rotational of the potential vector eq. ( 9). As result, the magnetic flux density presents two components, ܤ ሬԦ and ܤ ሬԦ ఝ , and the induced current only one component, ܬ Ԧ ఏ .

ܤ ሬԦ ൌ  × ܣ Ԧ ఏ , ܤ ሬԦ ൌ ቆ 1 ݎ ܣ߲ Ԧ ఏ ߲߮ ቇ ݑ ሬԦ ቆ- ܣ߲ Ԧ ఏ ݎ߲ ቇ ݑ ሬԦ ఝ ܤ ሬԦ ൌ -݆ ݇ ݎ ሺܥ ଵ ݎ ܥ ଶ ݎ ି ሻ݁ ሺఠ௧ିఝሻ ݑ ሬԦ ܤ ሬԦ ఝ ൌ - ݇ ݎ ሺܥ ଵ ݎ -ܥ ଶ ݎ ି ሻ݁ ሺఠ௧ିఝሻ ݑ ሬԦ ఝ (9) (10) (11) ܬ Ԧ ൌ ߪ ቆ- ܣ߲ Ԧ ఏ ݐ߲ -߱ ܣ߲ Ԧ ఏ ߲߮ ቇ ൌ -݆ߪܵሺܥ ଵ ݎ ܥ ଶ ݎ ି ሻ݁ ሺఠ௧ିௗఝሻ (12)
With the magnetic flux density given by ( 10) and ( 11) and the induced current density from (12), the magnetic force density in the rotor is computed as in (13). This shows the resultant force density having two components, a radial ܨ Ԧ and a tangential one

ܨ Ԧ ఝ . ܨ Ԧ ൌ ܬ Ԧ × ܤ ሬԦ ൌ ܨ Ԧ ܨ Ԧ ఝ ( 13
)
For motion applications, it is important to analyze the resultant average force density in the rotor and thus the average torque. This can be obtained as shown in ( 14) taking in account the active surface area of the rotor, its radius and the average force density in (15).

〈ܶ ఝ 〉 ൌ ݎ ඵ〈ܨ ఝ 〉 ݀ߠ ݀߮, 〈ܶ 〉 ൌ ݎ ඵ〈ܨ 〉 ݀ߠ ݀߮ (14)
ܨ〈 ఝ 〉 ൌ 1 2 ܴ݁൛ܬ መ ܤ * ൟ, ܨ〈 〉 ൌ 1 2 ܴ݁൛ܬ መ ܤ ఝ * ൟ (15)

Parameters' Sensibility

Figures 8 (a) and (b) show the dependence of the tangential and radial force density in the rotor in function of parameter k, which is the wavelength of stator's EMF. These results were obtained for a 5cm rotor radius with a 2mm thick aluminum material, a 2mm airgap and a stator current density of 6 × 10 ݉/ܣ ଶ (typical value of current density in electrical machines).

Results show that when increasing the wavelength of EMF (parameter k), both density forces magnitude are reduced, moving the maximum tangential density force to higher values of slip ܵ ᇱ . The radial component presents a repulsing force between stator and rotor.

Assistive Device Application

In this section it is analyzed the application of the shell-like actuator as an active joint for assistive devices. Application is a device for assistive movement of the lower leg for a typical 70kg person, usually used in orthopedics. Table 1 resumes the specifications of the active joint. For this purpose, the shell-like induction motor will have a simple design with a stator shell covering half of the rotor. This design warranties the range of motion in both Sagittal and Coronal planes. To study its feasibility, it was considered a 5cm radius rotor with a 2mm thick aluminum conducting material, a 2mm thick airgap, a 50 Hz stator current density of 6 × 10 A/m ଶ and k=4. For comparison, our design was simulated in 2D finite element method (FEM) program. FEM results are compared with the analytical solutions. For example, Figure 10 plots the resultant average torque obtained from the analytical model (continuous line) and that one determined using the FEM model (discrete marks).

The maximum torque obtained is about 4 Nm, therefore near to the specified one. The maximum angular velocity corresponds to 3.9m/s (78.5 rad/sሻ, including the average linear velocity of 0.83m/s (16.6 rad/s). This preliminary analysis indicates that the shell-like actuator design is capable of be the joint of the orthopedics assistive device.

Conclusions

The purpose of this paper is to study the feasibility of the shell-like induction machine, especially in assisting devices applications. The combination of the stator shell geometry and distribution of its coils allow a wide range of motion with multi-DOF. By the analysis of the potential vector with a simple model of the machine it was possible to extrapolate its behavior and the amplitude of forces possible for small sizes. Despite the simple model, it was possible to verify the parameter's influence on the main electromechanical characteristics. In addiction the FEM results obtained for a more realistic model, i.e., non-homogeneous geometry with non-simplified structure, were close to the analytical results.

The feasibility study concluded that this machine is capable of originating amplitude of torque needed in an orthopedic assistive device as the proposed leg joint.

Figures 1 (Fig. 1 .

 11 Figures 1 (a) and 1 (b) show the origin of the shell-like induction machine concept.The shoulder joint in Fig.1(a) is multi-axial and possesses the greatest range of motion of any human joint. Meanwhile, the hip joint of the anterior femur in Fig.1(b), it presents a shallower shell providing a lower range of motion. A geometrical representation of these joints is shown in Fig.2. Figure3illustrates the conversion of the biomechanical nature to a spherical and shell-like induction machine.

Fig. 2 .Fig. 3 .

 23 Fig. 2. Large and short range motion due to variable joint socket areas.

Fig. 4 .

 4 Fig. 4. Shell-like induction machine design.

Fig. 5 .

 5 Fig. 5. Cross section of shell-like induction machine

Fig. 6 .

 6 Fig. 6. Stator's windings geometry in cylindrical coordinates

Fig. 7 .

 7 Fig. 7. Boundary condition -Ampere's law in the a) stator and b) rotor.

Fig. 8 .Fig. 9 .

 89 Fig. 8. Influence of the EMF's wavelength in the density force components on rotor: (a) tangential component; (b) radial component. ܵ′ ൌ ሺ߱ -݇߱ ሻ ω ⁄ . Figures 9(a) and 9(b) indicate that the change of the rotor's electric conductivity has a similar effect as in classic induction machines. The maximum point of the force will be shifted to higher values of synchronism when decreasing the conductivity.

Fig. 10 .

 10 Fig. 10. Tangential component of the torque: analytical and FEM results.

Table 1 .

 1 Specifications for the orthopedic active joint.

	Total weight to lift with a 0.25m	2 kg (average lower leg
	distance to the center of mass	for 70 kg person)
	Average linear velocity	3 Km/h [0,83m/s]
	Range of Motion for Sagittal plane	[-10° 90°]
	Range of Motion for Coronal plane	[-25° 25°]
	Rated torque	5 Nm
	Range of radius	[2,5 5] cm

Acknowledgements. This work was supported by FCT, through IDMEC, under LAETA Pest-OE/EME/LA0022.


Rogério Campos-Rebelo

Anikó Costa

Luís Gomes

Elementary Events for Modeling of Human-System Interactions with Petri Net Models

Keywords: Petri nets, embedded systems, human-system interaction

This paper presents a proposal for structuring events for system models expressed using IOPT nets (Input-Output Place-Transition Petri nets). Currently, a non-autonomous event within an IOPT model is defined based on change of input signals with respect to a specific threshold, when two consecutive execution steps are considered. New types of events are proposed, allowing the definition of an event activated not only by crossing a fixed threshold, but also by considering a change in associated signal values on a specific amount (belonging to an interval of values). The concept is further extended allowing the definition of an event based on signal values presented on previous execution steps. The proposal results on a classification of several types of events, namely threshold events, momentum events, impetus events, as well as delayed events and logical events. Usage of these types of events allows improvements in terms of expressiveness and compactness of the resulted model.

Introduction

System complexity has grown considerably over the last decades. Some of the reasons for this growth are related with the increase in systems' processing capability and memory, as well as associated with the development of more robust technology. This complexity is due, mainly, to the need to produce more efficient systems, and more user friendly.

The growing development of the Service Oriented Architecture (SOA) and the Event-Driven Architecture (EDA) combined with the reduction of cost in sensor technology have led, in the last years, to a big development in the use of events in the analysis of signals and system' behavior [START_REF] Eckert | Complex Event Processing (CEP)[END_REF].

Use of event modeling allows the development of more complex systems expressed through a much more compact model, supporting the development of much more user friendly interfaces.

In order to cope with problems related with the system's complexity, several approaches were proposed to decompose the system development using multiple steps. Model Based Development approach, using specific languages for system specification, is one of these examples.

Graphical languages are normally recommended to support this approach. Some examples of graphical languages are statecharts [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF], state-machines [START_REF] Börger | Abstract state machines: a method for high-level system design and analysis[END_REF] or Petri Nets, which are used as reference modeling formalisms on this work.

The many developments that Petri Nets have suffered since its first presentation in 1962 [START_REF] Petri | Kommunikation mit Automaten (Communication with Automata[END_REF] have led to the growth of their use in various areas. One of those areas is engineering, taking advantage of some Petri net intrinsic features, such as the ability to model synchronization, concurrency, and conflicts [START_REF] Peterson | [END_REF], as well as the simultaneous visualization of the structure and behavior of the system [START_REF] Zurawski | Petri nets and industrial applications: A tutorial[END_REF]. These features allow Petri nets to capture the dynamics of the system, making them also useful in simulation [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF].

One of the issues that have taken a significant contribution to the growth of its use was the inclusion of non-autonomous characteristics. This has led to increasing the impact of their use, when compared to other modeling formalisms used for embedded systems design [START_REF] Gomes | Modeling Formalisms for Embedded Systems Design[END_REF]. These non-autonomous characteristics allow the connection of the net with the environment, making them well suitable for modeling the system's controller behavior.

Some examples of non-autonomous Petri net classes are the Interpreted Petri nets [START_REF] Moussa F | Interpreted Petri Nets used for Human-Machine Dialogue Specification in Process Control: principles and application to the Ergo-Conceptor+ tool[END_REF], synchronized Petri nets [START_REF] Moalla | Synchronized petri nets: A model for the description of non-autonomous sytems[END_REF] or IOPT nets (Input-Output Place-Transition nets) [START_REF] Gomes | The Input-Output Place-Transition Petri Net Class and Associated Tools[END_REF].

Whenever modeling human systems interactions are addressed, the number of available modeling primitives is limited.

Following the line of the work presented in [START_REF] Campos-Rebelo | On Structuring Events for IOPT Net Models[END_REF], this paper presents a more complete and elaborated set of elementary events, benefiting from a scalable definition, addressing the effectiveness of Petri nets modeling for human-system interaction systems, also keeping applications within the controllers' modeling.

Augmenting the traditional way to define an event (as a signal trespassing a threshold level), new ways to define an event associated with signal changes were proposed in [START_REF] Campos-Rebelo | On Structuring Events for IOPT Net Models[END_REF] related to amplitude and changing speed of variation on signal values.

In this work, this concept is extended allowing a generalized definition supporting the use of the specified signal variations.

On the other hand, for each variation level two different types of behaviors were previously defined. In this work, this definition is also extended.

Relationship to Collective Awareness Systems

Collective awareness systems are systems that allow interaction and knowledge development in collaboration by several people.

The work proposed in this paper presents a set of elementary events that are defined to be used in the future behavior definition based on events from one or more variables from one or more systems. These characteristics and its exact definition make them suitable for defining behaviors that can be shared or even set together.

On the other hand, the fact that the IOPT nets can be used to implement these events and these tools implemented online and interconnected in the same system ensures a greater capacity for development of collective awareness systems.

Signal Analysis

It is considered a signal as the value of a certain time variable. This variable can be physical or from the output of a system. As presented in [START_REF] Gomes | The Input-Output Place-Transition Petri Net Class and Associated Tools[END_REF], two ways can be considered to analyze a signal:

-Analysis of the signal value at a given moment in order to verify that this value meets a certain condition.

-Definition of events associated to that signal to analyze if the behavior of the signal in time obeys to the behavior that we want to find.

These two types of analysis are mainly different in terms of duration of the analysis. Whereas a condition is inspecting the value of the signal at a given instant of time. In an event, the behavior of the signal in time is analyzed.

From another point of view, a signal analysis can also be made taking into account different degrees of differences between consecutive values. The value of the signal, its derivative (considering two instants of analysis), its second derivative or the following derivatives can be analyzed. Given this analysis one can analyze not only a point or a variation between two points but also behaviors taking into account three or more instants on the signal.

In Table 1 these two types of dependencies on signal evolution is presented, showing the various possibilities for the analysis of a signal.

Table 1. Events and Conditions Definition

In terms of levels of variation (∆), defined as a difference of signal value in two consecutive instants, it is possible to define higher order of differences.

It can be seen that for all variations of X, the conditions only analyze a given value of signal X of the index n, while an event is analyzed based on the behavior between two index values n and n-1.

In the table, it can also check the possibility of analysis of the signal behaviors at various instants of the signal. Given that ∆X n = X n-1 -X n and ∆X n-1 = X n-2 -X n-1, an event in △X analyzes signal values in three instants (X n-2 , X n-1 e X n ). Likewise analyzing the event condition ∆ 2 X it has that ∆ 2 X n = ∆X n-1 -∆X n = (X n-2 -X n-1 ) -(X n- Table 3. Elementary Open Events definitions.

Pre-Condition

Post-Condition

X n-1 > K X n < K X n-1 < K X n > K X n-1 < K X n = K X n-1 > K X n = K X n-1 = K X n > K X n-1 = K X n < K
An elementary closed event can be analyzed taking into account only one of the conditions (pre or post-condition) in the two consecutive steps of analysis. For this kind of events, if the pre-condition was satisfied in the step n-1 and the same precondition is not satisfied in the step n, the event occurs because the post-condition is satisfied. For elementary open events, both conditions (pre and post) are needed to be analyzed.

To better understand, this type of events, it will be analyzed the event of the fourth row of the table, with the conditions X n-1 > K Λ X n = K. In this case, if the signal satisfies the pre-condition in instant (n-1), being greater than K and fails to satisfy this condition in instant n becoming less than K, while the pre-condition to be no longer satisfied the event does not occur. Thus, it is not possible to define this type of events using only one equation as proved possible for elementary closed events. It is not possible to define an elementary open event by composition of other events of the same type. This is the reason that makes it elementary. Despite this, being of another type, it is possible to define elementary closed events by composition of elementary open events.

Complete List of Elementary Events

With the previous definitions, it is possible to define a large number of types of events that define the behaviors of interest in the associated signal. Putting together the elementary open events and the elementary closed events a set of twelve types of events is obtained. A set of identifiers is used to represent events in a compact form.

The twelve events resulting from the merger mentioned above are defined for each of the various levels of variation (X, ∆X, ∆ 2 X, ∆ 3 X, …, ∆ n X). The Table 4 presents this set of events for X and ∆X, showing the conditions of the event and a graphical representation of the behavior of the signal that makes this event to occur.

For each level of variation, twelve types of events were defined, each one representing a specific behavior of the signal. These types of events are represented with a specific operator. In the variation level 0, the value of (X) is analyzed, detecting crossing of a specific value. For example, it is possible to define an event to detect if the temperature of the car is higher than 90 degrees. In variation level 1, the first difference (∆X) is analyzed, associated with the velocity of variation of the signal. For example, an event that occurs whenever the temperature of the car is increasing more than 5 degrees per minute can be defined. Finally, the other levels represent the next variations, starting with level 2, the second difference (∆ 2 X) (representing the acceleration of variation) up to level n represented by (∆ n X).

Delayed Analysis of Events

Until now, all events have been presented as analysis of variations in the signal between two consecutive steps of analysis (X n and Xn-1). Nevertheless, it is possible to set all these events and an analysis based on two distinct instants (not consecutive) separated by p steps of analysis (instead of one).

In this sense, delayed events are not a new type of events. They are a characteristic that can be changed in any type of elementary events. With the addition of this characteristic, the analysis of the event is done taking into account the values (X n e X n-p ). The analysis accomplished in the previous section is done considering two consecutive steps as a particular case where the value p = 1.

In Fig. 1 the way to analyze an event with delay is represented. To analyze this event a p-sized window is created and the signal inside this window is not used to the analysis of the event.

Taking into account the large number of types of events is not possible to use one single example to explain the full potential of these types of events. As a matter of fact, due to lack of space, it is not possible even to present a simple system's model taking advantage of any of these new modeling capabilities.

Conclusions and Further Work

The use of these new types of events provides effective modeling capabilities when using IOPT nets models. It allows the creation of smaller models for the same system, making them easier to read and easy to interpret.

The definition of different variations of the signal allows the analysis of a set of behaviors that allow a better knowledge of the signal, allowing not only changes on the value of the signal, but how these changes occurs, like its velocity or acceleration or even the acceleration of the velocity of the signal.

Taking into account the following objective to define events that represent more complex behavior of associated signs by composition of simple events, the definition of these elementary events becomes a robust starting point for this composition.

Those robust definitions allow the composition of events from different signals and even from different variations of the signal.

As future work, it is foreseen to define a set of transformations, as well as composition between elementary events in order to create a composed event. To do this, a standard compact representation for all elementary events and to the interaction between them needs to be defined.

Fig. 1 .

 1 Fig. 1. Analysis of a delayed Event.

Table 4 .

 4 Complete Elementary Events list

-X n ) and ∆

X n-1 = ∆X n-2 -∆X n-1 = (X n-3 -X n-2 ) -(X n-2 -X n-1 ). Thus in ∆ 2 X four values of the signal are analyzed (X n-3 , X n-2 , X n-1 e X n ).

Acknowledgments. The first author was supported by a Grant from project PTDC/EEI-AUT/2641/2012, financed by Portuguese Agency" FCT -Fundação para a Ciência e a Tecnologia".

This work was partially financed by Portuguese Agency" FCT -Fundação para a Ciência e a Tecnologia" in the framework of projects PEst-OE/EEI/UI0066/2011 and PTDC/EEI-AUT/2641/2012.

Elementary Events

An elementary event is defined as an event that cannot be obtained from the composition of other events of the same type.

In this work, two types of elementary events are determined that are distinguished by their behavior: elementary open events and elementary closed events.

Elementary Closed Events

Elementary Closed Events are events that define the analysis for the entire spectrum of signal values. In other words, any value that the signal can have satisfies one of the conditions of the event, either the Pre-or the Post-Condition.

An Elementary Closed Event is in such a way "Closed" that the event can be detected just by looking at one of the conditions. For instance, knowing that the signal satisfies a pre-condition at instant (n-1) and fails to satisfy this condition at instant n, it is guaranteed that he satisfies the post-conditions, which allows the detection of the signal without the need to analyze pre-and post-conditions.

In Table 2 the events defined with these characteristics are shown.

Pre-Condition Post-Condition

All events presented in the table are associated to value of signal X to simplify the presentation, but all these types of events can be defined in any ∆ n X.

Elementary Open Events

Elementary Open Events are events that do not define the analysis for the entire spectrum of signal values. In other words, there are values that the signal may have that are not covered by the equations that define the signal.

The Table 3 presents the defined set of types of elementary open events.


Rui Pais
email: ruipais@uninova.pt

João Paulo Barros

Luís Gomes

From SysML State Machines to Petri Nets using ATL Transformations

Keywords: ATL, Transformation Models, SysML, UML, State Machines, Petri Nets, PNML, MDE, MDA, IOPT

The ATLAS Transformation Language (ATL) is a well-known hybrid model transformation language that allows both declarative and imperative constructs to be used in the definition of model transformations. In this paper, we present ATL transformations providing an integrated structural description of the source and target metamodels and the transformation between them. More specifically, the paper presents translation rules of Systems Modeling Language (SysML) state machines models into a class of nonautonomous Petri net models using ATL. The target formalism for the translation is the class of Input-Output Place Transition Nets (IOPT), which extends the well-known low-level Petri net class of Place/Transition Petri nets with input and output signals and events dependencies. Based on this Petri net class, a set of tools have been developed and integrated on a framework for the project of embedded systems using co-design techniques. The main goal is to benefit from the model-based attitude while allowing the integration of development flows based on SysML state machines with the ones based on Petri nets.

Introduction

The increasing complexity of new-generation systems raises major concerns in various critical application domains, in particular with respect to the validation and analysis of performance, timing, and dependability-related requirements. Modeldriven engineering (MDE) [START_REF] Gasevic | Model Driven Engineering and Ontology Development[END_REF] approaches aimed at mastering this complexity during the development process have emerged and are being increasingly used in industry. They address the problem of complexity by promoting reuse and partial or total automation of specific phases of the development process.

By taking advantage of Petri nets visual representation and precise semantics, this paper contributes to their use as an intermediate formalism between SysML behavior models and code generation. More specifically, it presents a tool that transforms a Systems Modeling Language (SysML) state machine, to an Input-Output Place Transition Net (IOPT) [START_REF] Moutinho | Ecore Representation for Extending PNML for Input-Output Place-Transition Nets[END_REF] target model. The process of transformation  the production of an XMI [START_REF] Omg | OMG MOF 2 XMI Mapping Specification[END_REF] file  is realized using the Atlas Transformation Language (ATL) [START_REF]ATL -A Model Transformation Technology[END_REF]. The XMI file will be subsequently used as an entry to a Model Driven Architecture (MDA) [START_REF]OMG: MDA -The Architecture Of Choice For A Changing World[END_REF][START_REF] Barbosa | Checking Semantics Equivalence of MDA Transformations in Concurrent Systems[END_REF] process.

Present work benefits from the results of previous projects where a set of tools was created. These tools allow creation of IOPT net models, as well as many others operations. Ultimately, they also permit code generation for different platforms. Those tools rely on an Ecore metamodel for the IOPT class, already presented in [START_REF] Moutinho | Ecore Representation for Extending PNML for Input-Output Place-Transition Nets[END_REF].

Translation techniques to convert state machines elements into correspondent Input Output Place Transition Nets items were already presented elsewhere [START_REF] Pais | Towards Statecharts to Input-Output Place Transition Nets transformations[END_REF]. Later, these translations were extended to include other state machines elements and several strategies to translate state machines with pseudostate history attribute were also presented [START_REF] Pais | From UML State Machines to Petri nets -History Attribute Translation Strategies[END_REF].

This research extends previous works [START_REF] Pais | Towards Statecharts to Input-Output Place Transition Nets transformations[END_REF][START_REF] Pais | From UML State Machines to Petri nets -History Attribute Translation Strategies[END_REF] with the implementation of translation techniques, using ATL, to transform SysML state machine models to IOPT net models. The integration of these translations on a Petri net-based framework for the development of embedded systems using co-design techniques permits the use of SysML state machines as an additional modeling language.

The paper is structured as follows: Section 2 presents motivation, innovations and its relation to Collective Awareness Systems, while Section 3 describes some important concepts of Model to Model transformations. The implemented transformations rules using ATL are presented in Section 4. Finally, Section 5 presents topics for discussion and Section 6 concludes.

Relation to Collective Awareness Systems

An awareness system can be defined as a system intended to help people construct and maintain awareness of each other activities, context or status, even when the participants are not co-located [START_REF] Markopoulos | Awareness Systems -Advances in Theory, Methodology, and Design[END_REF].

As testified in [START_REF]Future Internet Enterprise Systems (FInES): Embarking on New Orientations Towards Horizon[END_REF], "Internet has changed the way we develop, perform and understand business", hence it is urgent to innovate and exploit the full potential of the Future Internet. To achieve this goal, a set of recommendations is provided and an analysis of important areas to consider is presented. More specifically, the analysis of Collective Awareness Platforms for Sustainability and Social Innovation (CAPS), points out that its basic layer includes (smart) objects that capture the environment reality. Many of these (smart) objects are embedded systems, which are frequently specified using Petri Nets. These are used for modeling and analyzing complex systems that exhibit characteristics of concurrency, synchronization, simultaneous, distributed, resource sharing, etc., taking advantage of tools that permit modeling visualization, simulation, property verification (e.g. deadlock, starvation, bottlenecks, and execution time), and code generation.

With this research, we contribute to the development of embedded systems allowing system specification using a well-known modeling formalism: SysML state machines. With better specification we are promoting better embedded systems, the core of smart objects.

Model to Model Transformations

Software development is becoming more and more complex with the increasing complexity of system requirements, necessity to integrate frameworks, libraries, communication platforms, etc.

Maintenance, changing requirements, production cost, specification reusability, and a lot of other factors contribute to a demand to improve software specification. One way to reduce technical complexity is the use of the Model-Driven Software Development paradigm, as it facilitates a more abstract specification of software based on modeling languages [START_REF] Lochmann | HybridMDSD: Multi Domain Engineering with Model Driven Software Development Using Ontological Foundations[END_REF].

In the context of model-driven engineering, models are the main development artifacts and model transformations are among the most important operations applied to models. Model-to-model transformations constitute an important ingredient in model-driven engineering.

The following sections present the main concepts used in this context.

Ecore

The model used to represent models in the Eclipse Modeling Framework (EMF) is called Ecore. Ecore is itself an EMF model, and thus is its own metamodel [START_REF] Steinberg | EMF: Eclipse Modeling Framework[END_REF]. Ecore is a modeling language (in fact a meta-meta-modeling language) to describe domain specific meta-models. It is used to define all entities that will exist on the domain specific models of interest, define the characteristics of these entities, as well as their relationships.

ATL Language

The ATLAS Transformation Language is a model to model transformation language originally developed as a response to the Object Management Group (OMG) Request for Proposals for the Query/View/Transformation (QVT) standard [START_REF]OMG: Meta Object Facility (MOF) 2.0 Query/View/Transformation Specification[END_REF], implemented in the Eclipse modeling tools.

ATL is a well-known hybrid model transformation language that allows fully declarative, hybrid, or fully imperative constructs to be used in transformation definitions.

An ATL transformation is unidirectional and operates on read-only source models to produce write only target models. This way, source model can be navigated during transformation, but it is neither possible to write on the source model, nor to navigate target model. Yet, ATL provides automatic traceability links between target and source elements.

ATL model transformation process is illustrated on Fig. 1. This provides an overview of the transformation process used for the generation of an IOPT model (IOPTnet.xmi) from a SysML state machine model (StateMachine.xmi) through a transformation model (SM2IOPT.atl). In this diagram, the dotted line specifies model to model transformation; the normal arrows specify conformance between source state machine model (StateMachine.xmi) and its metamodel (StateMachine.ecore), as well as between this metamodel and the Eclipse Modeling Framework (EMF) metametamodel. On the same way, the generated model (IOPTnet.xmi) conforms to its metamodel (IOPT.ecore), and the latter conforms to the EMF metametamodel.

SysML State Machines

The Systems Modeling Language (SysML) is a general-purpose modeling language that supports the specification, analysis, design, verification, and validation of a broad range of complex systems, which may include hardware, software, information, processes, personnel, and facilities [START_REF]OMG: OMG Systems Modeling Language[END_REF]. The respective State Machine package defines a set of concepts that can be used for modeling discrete behavior through finite state transition systems [START_REF]OMG: OMG Systems Modeling Language[END_REF].

Input-Output Place Transition Nets

Petri nets have been successfully used for concurrent systems specification [START_REF] Choppy | A Modelling Approach with Coloured Petri Nets[END_REF] for the analysis of behavioral properties and performance evaluation, as well as for systematic construction of discrete event simulators and controllers [START_REF] Zurawski | Petri Nets and Industrial Applications: A Tutorial, Industrial Electronics[END_REF].

The Input-Output Place Transition class (IOPT) extends place-transition nets with non-autonomous constructs, allowing explicit modeling of input and output events and signals [START_REF] Moutinho | Ecore Representation for Extending PNML for Input-Output Place-Transition Nets[END_REF]. The Ecore metamodel for the IOPT net class was already presented in [START_REF] Moutinho | Ecore Representation for Extending PNML for Input-Output Place-Transition Nets[END_REF][START_REF] Ribeiro | An Ecore based Petri Net Type Definition for PNML IOPT Models[END_REF].

Transformations Rules using ATL

In this section, we present a set of transformation rules and helpers that allow the generation of IOPT models from SysML state machines models. The result of each transformation is an XMI file on PNML format. Some translation techniques to convert state machines elements into correspondent Input Output Place Transition Nets items were already presented elsewhere [START_REF] Pais | Towards Statecharts to Input-Output Place Transition Nets transformations[END_REF][START_REF] Pais | From UML State Machines to Petri nets -History Attribute Translation Strategies[END_REF]. The respective implementations are here presented. Yet, as the transformation application is extensive, we only show some code blocks, representative of interesting transformation aspects.

Transformation rules are the core of a model transformation. A transformation rule can be implemented with declarative, fully imperative, or hybrid constructs.

The declarative style of specifying transformations are encouraged as best practice [START_REF] Allilaire | ATL -Eclipse Support for Model Transformation[END_REF], letting imperative features of the language to the most complex transformations when declarative constructs are not sufficient.

Declarative transformations rules use pattern matching to match the source model elements by type. A rule guard permits an additional filtering on pattern matching. For each matched element one or more target model elements are created.

Transformations traceability is an important language feature that offers trace links between source and target models, and between rule applications. This is important, as it allows one rule to reference elements created in other rules.

The matching rule 'package2PetriNetDoc' is one of simplest transformation rule. For each source model element of type 'Package' it collects the traceability links generated by target pattern 'net'; it uses the imperative parts 'using' and 'do' for debug proposes. For each source model element of type 'Package', this rule creates a target 'PetriNetDoc'. This rule uses the 'allStateMachines' helper that is presented later in this paper.

To illustrate and exemplify the implemented translations, we present the translation of state machine choice pseudo-state.

A choice pseudo-state has one incoming and several outgoing edges, and it is used as a switch of control flow based on zero or more guard condition. Depending on the guards' conditions, the control flow is redirect from one incoming edge to exactly one outgoing edge. Fig. 2 presents a simple state machine with a choice pseudo-state, and Fig. 3 presents its translation to an IOPT net. This translation was implemented by three main rules: 1. One rule that translates state machine states to IOPT places; 2. One rule to translate state machine choice guards; 3. One rule to translate state machine choice state to a set of IOPT transitions and arcs. This last transformation rule is presented next.

Matching rule 'choicePseudostate' transforms a source 'choice pseudo state' into a set of target model transitions, a set of input arcs, and a set of output arcs. This rule calls various 'unique lazy rules' to generate arcs on target models. The 'using' declarative part allows the declaration of variables that increase code legibility by giving names to different elements used in transformations.

---join vertices serve to merge several transitions emanating ---from source vertices in different orthogonal regions. Helpers can be used to define attributes, constants, and methods like functions. They can be reused throughout several transformations and in different contexts as utility functions, rule guards, and model properties analysis, as well as to navigate the source model. A task that is common to many transformation examples is the definition of helpers to get all elements of a specific type. Next, we present some of these helpers.

(1) Helper 'allStatesMachines' gets all state machines from a source model.

---helper to get all statemachines helper def: allStateMachines: Set(SysML!StateMachine) = SysML!StateMachine -> allInstances();

(2) The matching between source models elements and transformation rules is defined by conditions guards defined on rules level. As these conditions are normally extensive, we have created guard helpers to increase overall legibility. Helper 'isJoinPseudostate' is a simple guard helper that verifies if vertex element is a pseudostate of the 'join pseudo state' kind. In a complete state machine, a join vertex must have at least two incoming transitions and exactly one outgoing transition [START_REF]OMG: Unified Modeling Language TM (OMG UML)[END_REF].

---Verify if pseudostate is of kind 'join pseudo state' helper context SysML!Vertex def: isJoinPseudostate(): Boolean = self.oclIsTypeOf(SysML!Pseudostate) and self.kind = #join and self.incoming->size() >= 2 and self.outgoing->size() = 1;

(3) Transforming elements from source model to target model, normally, doesn't depend only on the kind of source item, but also on the context where it is inserted and/or on the context of interconnected elements. It was necessary to create a vast number of functional helpers to navigate interconnected elements and to obtain the necessary collections or properties. Functional helper 'getOwners' gets all owners of context element, which can be of any type, and returns a sequence of all owners from context element to root item.

Discussion

When implementing a translation from a source model to a target model, it is necessary to create rules that match source elements and generate target elements. When there is no clear relation between them, it is not easy to identify which elements from source should be used, and which matched element should be generated.

Currently ATL has four compilers: 2004, 2006, 2010, and EMF Transformation Virtual Machine (EMFTVM). Present research was implemented with compiler version 2010, which has important limitations on traceability (tracing mechanism), not permitting the use of all types of rules as they lack the tracing mechanism. Moving to EMFTVM, which has advanced language features, will allow some code improvements. ATL documentation is spread along Eclipse ATL site, wikis, papers, and forums. A book or some other documentation explaining "How to do transformation" and not "How to use methods/functions" is missing. Even so, using ATL as a model to model transformation language simplified all the translation process, allowing an emphasis on translation technics in opposition to programming languages issues. Preliminary results, allow us to conclude that the strategy to convert Behavior Models to Petri Nets is possible and of great interest to strengthening the assertion of Petri Nets as a formalism suitable for integration of models.

Conclusions and Future work

The implementation of all transformations between SysML state machines and IOPT nets is a significant contribution to be added to the framework for the project of embedded systems using co-design techniques. It is now possible to go from SysML state machines to IOPT nets, verify their properties, optimize the model, generate code, visualize, and execute. As an overall view of the implementation, it is interesting to note that 80% of all transformation rules were implemented using the declarative language style, recommended as best practice [START_REF] Allilaire | ATL -Eclipse Support for Model Transformation[END_REF]. The use of variables on the imperative 'using' rules part, rule guard helpers, and called rules, allowed an overall good code readability. As near future work, it is necessary to enhance understandability of transformations and improve their correctness, which will lead to the identification and analysis of the used modeling patterns, as well as refactoring and abstraction mechanisms on model to model transformations. Finally, formal techniques for checking semantics equivalence of MDA transformations [START_REF] Barbosa | Checking Semantics Equivalence of MDA Transformations in Concurrent Systems[END_REF] can be used to validate implemented transformations.

Fig. 1 .

 1 Fig. 1. ATL Model Transformation (adapted from [21])

  !Package(inn.isPackage()) using { ruleName:String= 'package2PetriNetDoc'.debug('!Starting); } to petriNetDoc : PNML!PetriNetDoc( nets <-thisModule.allStateMachines->collect (p | thisModule.resolveTemp (p, 'net')) ) do { ruleName.debug('!Ending rule'); } }

Fig. 2 . 3 .

 23 Fig. 2. State machine with choice pseudo-state Fig. 3. Translated IOPT net

  Previous helper 'getOwners' is used by various helpers to determine its relation of inclusion with other types of items. Helper 'isInsideCompositeState()' is one of these examples: it verifies if a transition is inside a composite state, which means that it must be inside of a composite state with or without a region inside it. This helper calls helper 'isCompositeState()' to determine if SysML element is of the composite state kind.

	---Verify if a transition is inside a composite state
	helper context SysML!Transition def : isInsideCompositeState():
	Boolean =
	let elements : Sequence(SysML!Element) = self.getOwners() in
	if(elements.size() >= 2) then
	elements.at(1).isCompositeState() or
	elements.at(2).isCompositeState()
	else
	elements.at(1).isCompositeState()
	endif;
	---Get all owners of a given element
	helper context OclAny def: getOwners(): Sequence(SysML!Element)=
	let itemOwner : SysML!Element = self.owner in
	if self.oclIsUndefined() then
	Sequence {}
	else
	if(itemOwner.oclIsKindOf(SysML!Element)) then
	Sequence {self}->union(itemOwner.getOwners())
	else
	Sequence {}
	endif
	endif;


José-Inácio Rocha
email: jose.rocha@estsetubal.ips.pt

Octávio Páscoa Dias
email: octavio.pdias@gmail.com

Luís Gomes

Keywords: Dataflows, Petri nets, Synchronous Dataflows, Place and Transition Invariants, Models of Computation

Over the last decades a large variety of dataflow solutions emerged along with the proposed models of computation (MoC), namely the Synchronous Dataflows (SDF). These MoCs are widely used in streaming based systems such as data and video dominated systems. The scope of our work will be on consistent dataflow properties that can be easily demystified and efficiently determined with the outlined mapping approach between Dataflows and Petri nets. Along with this strategy, it is also highlighted that it's of a major relevance knowing in advance the proper initial conditions to start up any SDF avoiding buffer space over dimensioning. The methodology discussed in this paper improves the outcomes produced so far (in Petri net domain) at design stage aiming at knowing the amount of storage resource required, as well as has a substantial impact in the foreseen allocated memory resources by any signal processing system at the starting point and also points out new directions to minimize the buffer requirements at design stage.

Introduction

Over the last decades a multitude of dataflow solutions emerged along with requirement always supported by the needs of each new Model of Computation subtleties and peculiarities. Researchers have developed a few number of dataflow variants, trying to model the different constraints presented in the firing rules. These constraints about the firings rules are what differentiate several developed MoCs. For example in Cycle-static Dataflow [START_REF] Bilsen | Cycle-static dataflow[END_REF], tokens rates can be scheduled in a periodic way, while in Dynamic Dataflow [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF] token rates can be changed after each schedule. Another variant called Parameterized Synchronous Dataflow [START_REF] Bhattacharya | Parameterized Dataflow Modeling for DSP Systems[END_REF] allows the tokens rates to be defined by a parameter, which can be changed only between schedules. Synchronous Dataflow (SDF) is a Model of Computation where the number of tokens consumed or produced by an actor is known in advance at compile time, i.e. without executing the model. This way, a SDF can be viewed as a statically schedulable model [START_REF] Lee | Static Scheduling of Synchronous Data Flow Programs for Digital Signal Processing[END_REF]. Every SDF model is composed by nodes and arcs (also usually called edges or channels). The nodes (graphically correspond to circles or ellipses) represent the functional or activity elements, while the edges (symbolized by arrows) represent communication channels between them. These channels are conceptually first-in-first-out queues. Edges are tagged with weights appended on both ends by non-negative integers. Due to their activity nodes consume and produce an establish amount of tokens on each firing based on tagged weights in the arcs. Tokens (represent by black dots) can also be seen as delays; therefore edges may contain initial markings which correspond to an initial number of delays. SDF model have demonstrate their adequacy in many signal processing and multimedia domains, in which there is no data-dependency in each schedule, i.e. the tokens rates remains constant after each actor firing, therefore the rates of tokens are fixed by nature. But this weakness (lack of expressiveness) can be viewed as its strength, since it's possible to analyze all models for deadlock or bounded buffers. Several advantages can be outlined to SDFs models, namely the easiness in modeling signal processing multi-rate systems, the ability to generate static schedule at compile time (allowing to know the required resources in advance), and the sequential static schedules can be optimized for buffer memory minimization, as well as allowing efficient simulation and efficient code generation. In a nutshell, SDF are wellmatched to signal processing and communications systems. In [START_REF] Rocha | Petri net verification techniques on synchronous dataflow models[END_REF] and [START_REF] Rocha | Exploiting Dataflows and Petri Nets Mappings[END_REF] the researchers aimed at unveiling the effective and potential maximum number of tokens for each arc in every Synchronous Dataflow to foresee at compile time the necessary amount of storage resources, i.e. at design stage, as well as the study of dataflow models under a cyclic and continuous flow of data, whereas in this paper new developments are highlighted in the scheduling analysis and on reducing the allocated buffer memory by buffer sharing.

The paper is organized in seven topics. After a short introduction and motivation about dataflows, a brief discussion about the issue under investigation in the present paper to the relationship to collective awareness systems is outlined. In a nutshell, the state of the art provides an overview upon the matter under research. Section 4. ("The proposed methodology") presents and depicts the basic ideas behind the mappings outlined between dataflow and Petri net domains. Experimental work and results are shown in section 5. In section 6 it is presented in a summarized way the tools and computational environments used to work out the conclusions. The paper ends up with some guidelines that will rule the further research work on the key area of interest.

Relationship to the Collective Awareness Systems

Collective awareness is an issue that is nowadays being addressed in existing literature by several researchers due to the need to improve the knowledge of the impact of the different scenarios that are growing mainly on the side of the technological "footprint". The need to seek for understanding at what surround us, which make us above all a social creature, is demanding a worldwide coordination and awareness to gather in a more fruitful way all these new collaborative emerging realities.

The proposed approach in this document maintains a close regarding to collective awareness and aims its future research to a subject which is a topic being conveyed as a worldwide awareness (a wide collective awareness) in terms of earth's sustainability, the optimization energy consumption in order to fulfill very tight power requirements demanded by a target application or an embedded system. It is a vital subject since our society is founded on energy and due to increasing demanding on portable electronic devices and massive utilization, optimization of power (energy) consumption has become a critical design point. The industry of low power consumer electronics is currently submitted to a huge growth, while the power dissipation of digital systems experiences an increase in device density, complexity and speed, and the last but not the least the growing interest in lower power chips and systems are driven by business and demanding technical needs. Researchers and system developers are aware of the tradeoff between power and performance [START_REF] Gary | Practical Low Power Digital VLSI Design[END_REF]. Moreover, tools and strategies can be developed or improved to go on even further to pursue the goal of devising optimized applications and embedded systems on different platforms. Memory resources are scarce in every signal processing system, therefore the contribution of tools to ameliorate this topic are of great significance nowadays when used together with the lowest sleep and active power draws hardware techniques. Our approach intends to be a contribution aiming at knowing the minimal allocated resource memory even at and during a system's startup period.

Summarized Overview of the Supporting Formalisms

Actually Embedded Systems have a multitude of constraints and non-functional requirements, as a result to perform the synthesis or code generation efficiently of models the practitioner must deal with several issues, ranging from energy constraints, buffer requirements, memory efficiency and performance. To deal with these matters, two modeling formalisms are used in this work: Dataflows and Petri nets. In order to present Dataflows and Petri nets a summarized overview is provided, for a more complete and formal descriptions of Petri nets see for example [8, 9 and 10] and for Dataflows see [11, 12 and 13].

Dataflows

The basic idea of the principles of a language for parallel processing outlined by Gilles Kahn [START_REF] Kahn | The Semantic of a Simple Language for Parallel Programming[END_REF] in his seminal paper was to represent programs using nodes and arcs. Later on, Dennis [START_REF] Dennis | First version of a data flow procedure language[END_REF] established the dataflow principles aiming at exploitation of parallelism in programs. In a dataflow, nodes are associated to computational program activity, and arcs connecting nodes convey the flow of information. Arcs are First-In-First-Out queue channels with blocking read operations and non-blocking write operations. Lee et al. [START_REF] Lee | Synchronous data flow[END_REF] presented in 1987 a special kind of dataflow known as Synchronous Dataflow (SDF) where the token rates (incoming and outgoing) are fixed and established by nodes on each arc, thus improving the runtime overhead of the modeled system. Nowadays SDFs are a mature approach and are well disseminate among stream based system, namely parallel and distributed signal processing systems, since one can detect deadlocks at compile time, as well as have demonstrate their adequacy in specifying multirate systems that can be statically scheduled. Figure 1 (a) illustrate a SDF model where some arcs contain black dots representing initial markings (which can also be known as tokens or delays).

Petri Nets

A Place-Transition Petri net is a special bipartite directed graph (consisting of two kind of nodes, places and transitions), and can be viewed as a graphical and mathematical modeling tool. As a graphical tool, Petri nets are a valuable tool since they can be used as a visual aid to simulate the concurrent and dynamic activities of the systems. As a mathematical tool, it is possible to address algebraic equations, state equations and other mathematical formalisms that govern the system's behavior and structure. The origin theory of Petri nets is based on the work of Carl Adam Petri dissertation's published in 1962. Graphically, places are drawn as circles or ellipses, and transitions as bars or rectangles. Arcs are tagged with positive integers representing weights, and are either from a place (/transition) to a transition (/place). Places may hold tokens defining the state of the system. In the graphical environment tokens assigned to places correspond to black dots or positive integer numbers. The activity of Petri nets is ruled by enabling and firing transitions. In a word, a transition is enabled if each input place is marked with a minimum number of tokens fixed by the arc weight, and whenever enabled the transition will eventually fire. In figure 1.

(b) one can see an example of a Petri net model.

The Proposed Methodology

The fundamental idea of our methodology is to make use of an inter-relation between a Synchronous Dataflow (SDF) and a transformed equivalent Petri net (PN). The idea was first presented in [START_REF] Rocha | Dataflow Model Property Verification Using Petri net Translation Techniques[END_REF]. This way one can encompasses and take benefit from the well known properties verification capabilities of Petri nets, namely invariants and reachability analysis. Based on this inter-relation between SDF and PN, valuable information is added to the scheduler allowing one to gain insight knowledge about the storage resource in each arc, as well as the resource allocation of the whole SDF by realizing an inverse mapping into dataflow domain. The complete mapping strategy is depicted in figure 2. In a summarized way, one tries to find a relationship between every element in each domain, keeping in mind that each of these environments due to its nature has passive and active elements. This way, a process/function (represented by a circle) in a dataflow corresponds to a transition in Petri net domain (depicted by a bar). Since arcs in dataflows represent paths that conveys the oriented stream of information, arrows are used between the processes. The matching element on the Petri net side for the oriented path is a circle, embodying normally conditions, states, resources or objects. Arcs in a dataflow also include weights and initial markings denoted by non negative integer tagged at both ends of the arrow and black dots, respectively. The previous two characteristics find their matching elements in the lower part of figure 1, on the side of Petri net domain. To illustrate our approach, a dataflow is presented in figure 1 (a) and the corresponding equivalent Petri net model is shown in figure 1 (b).

A Petri net with m places and n transitions is represented by a matrix (mxn) called the incidence matrix C. The entries of the incidence matrix are integers representing the token balance associated to the firing of every transition in the Petri net. If there is token gain the numbers are positive, for a loss and no change on the associated transitions, negative and zero entries in C are used respectively. This matrix is the key element to establish the transition or fundamental equation which governs the new markings on the Petri net given an initial marking set. Based on a qualitative analysis of PN two properties support our analysis: (1) Place Invariant (P-Invariant); and (2) Transition Invariant (T-Invariant). Based on the incidence matrix one creates a set of homogeneous linear equations which allows finding the so called P and T-Invariants. The structural domain analysis is aimed at designing systems without any kind of inconsistencies coping with properties which stay constant during model's execution. Maximum potential number of tokens is computed with P-Invariants, as presented in [START_REF] Rocha | Analysing Storage Resources on Synchronous Dataflows using Petri Net Verification Techniques[END_REF], whereas the maximum effective number of tokens on each arc in a dataflow is achieved summing all values presented in the reachability tree. More over with T-Invariants one can foresee the potential initial markings (M0) for each place. Using the reachability tree one can keep track of the maximum number of tokens present on each arc during a schedule. This way the buffer size for each individual arc is foreseen on the dataflow. Gathering all these values the total buffer requirements for the arcs present in a dataflow is estimated. The spectrum actor in figure 3 requires multiple input tokens to fire. This input multiplicity is established by a parameter called order, which is always a number dependent of power 2. The icon "SDF Director" governs the proposed dataflow model by defining the number of iteration to be performed and additionally determines the number of times each actor fires in one iteration using the balance equations. The multi-rate SDF model presented in figure 3. (a) is called well ordered chain structured SDF, and for these cases it is necessary to add an extra place (p3) to make the whole Petri net reversible and live (for further reading see [START_REF] Murata | Petri Nets : Properties , Analysis and Applications[END_REF]), because at the end of each periodic schedule the digital signal processing system exhibits cyclic behavior since there is always an imbalance in the number of tokens. Besides this condition is central to evolve our methodology which is based on the P/T-Invariants in Petri net domain (see [START_REF] Rocha | Exploiting Dataflows and Petri Nets Mappings[END_REF]).

Experimental Work and Results

One may argue that the reachability tree is a bottleneck due to the state space explosion problem; however, it is possible to distribute the state space in a set of computing machines [START_REF] Murata | Petri Nets : Properties , Analysis and Applications[END_REF] limiting this drawback. The experimental work was carried on two kinds of (well-known) problems, the dining philosophers and distributed database, besides the process is still dependent on the choice of having a good hash function to guarantee also a good state's distribution among the processors.

Scheduling Analysis of Synchronous Dataflow

Analysis of ill-specified SDF at the design time or even the misbehaved ones is an issue of major relevance. In a SDF our concern is related to attain a static schedule (if one exists), where a finite periodic list of actors is schedule in a sequential way. A SDF can evidence either rate-inconsistency (motivated by unbounded memory problems), or inability to run, or even deadlock caused by lack of initial buffering. As stated in Lee et al. [START_REF] Lee | Static Scheduling of Synchronous Data Flow Programs for Digital Signal Processing[END_REF] "a periodic admissible sequential schedule (PASS) is a periodic and infinite admissible sequential schedule", one concludes that after a period has been executed, the size of each buffer returns to its initial state, i.e. or to its home state (as it is known in Petri net domain).

To illustrate our idea considers the following flowchart depicted in figure 4. Taking the equivalent Petri net model one can identify easily if either a SDF model is consistent or inconsistent, or has deadlocks, using the P-T Invariants (structural analysis) and the reachability tree (behavioral analysis). Therefore, it is possible to draw a methodology (on the side of Petri net domain) for each and every SDF to find out their runnability feature. Figure 5 presents all those cases of runnability in SDFs models. The use of the reachability tree can be seen as a bottleneck by some researchers due to the state space explosion problem; however it is possible to distribute the state space in a set of computing machines [START_REF] Boukala | Towards distributed verification of petri nets properties[END_REF] limiting this drawback. Additionally to know the real impact of the initial conditions in the spectrum analyzer multiple simulations were performed using the computational environments to estimate the number of states generated, as well as the number of fired transitions in the foreseen static schedule. Observing Table 1 among the various cases identified one (case 1) conducts the system to a minimum in the number of states and fired transitions. Therefore from the other cases in Table 1 one can conclude that initial conditions (in place p1 and p4) will make the modeled system progress to some extra states that are not relevant for the periodic static schedule, thus augmenting the state space and at the same time unnecessarily over dimensioning the system. Thus it is important to develop an algorithm to find out the initial conditions that conduct the modeled system to a minimal state space and also reduces the required storage space.

Reducing Buffer Memory by Buffer Sharing

In order to reduce even further the allocated buffer space among the arcs it is important to unveil those that don't overlap their live ranges stressing that each arc is committed to a First-In-First-Out (FIFO) buffer. The strategy to follow is to observe the way each place in each state behaves traversing the state space of the schedule and then, decide what are the places that don't overlap at each state by grouping those that are disjoint in state space schedule. After this identification one is able to state which buffers can be fully shared. To illustrate our methodology, an example is used, the spectrum analyzer. The corresponding SDF is shown in figure 6. (a). The equivalent Petri net model of the spectrum analyzer (in figure 6. (b)) is used as an example to illustrate the issue of the buffer sharing. This way the following buffer sharing is possible: places p0, p1, p2 and p3 can share the same buffer and requires a buffer size of 4 units, which is the maximum amount of storage in this subset of places; places p4 and p5 can also share the same buffer and require a buffer with unitary dimension; and finally place p6 needs a buffer of 4 units. Summing the contributions of each group of shared places one attains the total amount of buffer space of 9 units, representing a space memory saving of 47 percent in comparison to the initial solution.

Tools and Computational Environments

The development of the equivalent transformed Petri nets was performed by two non commercial tools that are freely available in the web: (1) Integrated Net Analyzer INA [START_REF]INA -Integrated Net Analyser[END_REF], a non graphical Petri net editor, that requires a previous knowledge of the INA syntax language to perform a net description; (2) Still TINA -TIme Petri Net Analyzer [START_REF]Laboratoire d'Analyse et d'Architecture des Systémes[END_REF], a graphical editor with a stepper simulator to perform a step by step animation in a Petri net. The invariant analysis (used in section 5) was performed in both environments.

Conclusions and Further Work

The proposed methodology allows one start from a dataflow model, a Synchronous Dataflow, and based on a set of mapping rules achieve an equivalent Place -Transition Petri net model exploring the well-known verification properties: Behavioral (Structural) properties which are dependend (independent) on the initial marking. In this paper the focus is on the behavioral properties: reachability, boundedness, deadlocks, liveness, reversibility and home state. Using reachability tree one can identify if from a initial marking it is always possible to reach that initial state (referred in this case as home state), or know the firing sequence that brings the equivalent Petri net to the home state. Boundedness was useful to get the required buffer space for each Synchronous Dataflow arc and reveal if no design errors were committed at design stage. Liveness is a major property for the stream based SDF models since data flows sequentially, continuously and iteratively since ones tries to find a schedule, i.e., guarantee the absence of deadlocks. On the side of structural properties the analysis is focused on the invariants (P and T) to achieve the buffer (token) capacity concerning each arc in SDF models. Initial conditions in dataflow models play an important role since with the proper initial conditions the system will not be over dimensioned, which are not desirable and should be avoided. Moreover, choosing different initial conditions one can state and conclude that the modeled system will evolve to some states that are not relevant for the periodic static schedule, thus augmenting the state space will jeopardize (more time consuming task) the search for specific states, such as for example the home state. In resume, the goal is to look for initial markings that make system runnable to complete periodic static schedules. As future work, one should find an algorithm to identify amongst all firing conditions those that lead the system to a minimal state space encompassing a finite periodic static schedule using the modeling formalism of PN. Also outline an algorithm (or an optimization algorithm) to find regions (or sub-regions) in the state space where a buffer sharing may be possible. This strategy will allow reducing to a great extent the buffer requirements.

1 .

 1 An example of a Dataflow model, where some arcs contain initial tokens (a) and Petri net model (b).

Fig. 2 .

 2 Fig. 2. Proposed mapping between dataflow and Petri net domain

Fig. 3 .

 3 Fig. 3. An implementation of a multi-rate SDF Dataflow model in Ptolemy environment (a) and Petri net equivalent model supported by the translation rules presented in Fig. 2.

Fig. 4 .

 4 Fig. 4. Flowchart to identify the runnability (or rate consistency) of SDFs As another example consider the simplified spectrum analyzer dataflow presented in figure 6 (a) and based on the translation rules outlined in section 4. one can get the Petri net model shown in figure 6 (b).Using the Petri net structural analysis, it is possible to know the maximum potential and effective amount of storage space for the static schedule identified, as stated before. The amount of storage space for each arc (M(pi) stands for the number of tokens in place pi) are shown in figure7(a) and the associated static schedule in figure7 (b). The total buffer requirement for the spectrum analyzer is 17 units, where each arc in dataflow domain maps to a place in Petri net domain. In the reachability tree achieved under Petri net domain one must find the home state in order to know the execution time of the periodic static schedule and at the same time can observe the execution pattern of each process in a single schedule as shown in figure7 (b). If every process (transition) takes 2 time units, the entire schedule execution time will take place in 18 time units. From figure7(b), one can observe that in every periodic static schedule the Adaptive LPF (ALPF) process executes 4 times, FFT Zoom (FFT Z), Peak Detector (PD), Interpolator (INT) and Zoom Control (ZC) executes one time and that Decision (DECI) executes 2 times. The use of the reachability tree can be seen as a bottleneck by some researchers due to the state space explosion problem; however it is possible to distribute the state space in a set of computing machines[START_REF] Boukala | Towards distributed verification of petri nets properties[END_REF] limiting this drawback. Additionally to know the real impact of the initial conditions in the spectrum analyzer multiple simulations were performed using the computational environments to estimate the number of states generated, as well as the number of fired transitions in the foreseen static schedule.

Fig. 5 .Fig. 6 .

 56 Fig. 5. Synchronous Dataflows and their equivalent Petri net models for different runnability cases; (a) rate consistent with bounded memory; (b) rate-inconsistent with unbounded memory; (c) rate-inconsistent -cannot run; (d) rate consistent with deadlock; (e) rate-consistent without deadlock.

Table 1 .

 1 State space and fired transitions for several cases for different initial marking on places p1 and p4 (M0(p1) and M0(p4)), for figure 6 (b).

	Case	M0(p1)	M0(p4)		# states			# fired transitions
	1	4		1		20			32
	2	4		2		31			56
	3	8		1		68			144
	4	8		2		114			276
	5	5		1		28			50
	6	7		1		52			106
	M(p0)	M(p1)	Amount of storage space per arc M(p2) M(p3) M(p4)		M(p5)	M(p6)	Total
	4	4	1		2	4		1		1	17
					a)
					Time stamp
	Schedule	1	2	3	4	5	6	7	8	9	10
	1	ALPF,	ALPF	ALPF	ALPF	FFTZ	PD	INT	DECI	DECI
		ZC
	2										ALPF
											,ZC
					b)
	Fig. 7. Buffer requirement for a periodic static schedule of spectrum analyzer dataflow (a), and
	the corresponding static schedule (b).

Acknowledgments

This work was partially financed by Portuguese Agency "FCT -Fundação para a Ciência e a Tecnologia" in the Framework of projects PEst-OE/EEI/UI0066/2011 and PTDC/EEI-AUT/2641/2012 and by Instituto Politécnico de Setúbal (IPS) in the framework of projects of "3º Concurso de Projectos do IPS", reference 3CP-IPS-8-2009.