Quality-of-Service mechanisms are required for the transmission of flows with different criticality levels on a real-time Ethernet network. Static Priority Queueing (SPQ) is such a popular mechanism since it can bound the impact of lower-criticality flows on higher-criticality ones. To ensure deadlines for critical flows, several worst-case traversal time (WCTT) analysis methods have been proposed for SPQ. However, they compute pessimistic upper bounds on delays, causing unnecessary network over-dimensioning. This paper identifies and analyses the sources of pessimism in Network Calculus based WCTT analysis under SPQ. We also propose a method to construct near-worst-case delay scenarios within a tractable search space, enabling estimation of an upper bound on pessimism. Our results reveal a significant gap between computed upper bounds and attainable near-worst-case delays, paving the way for improvements in WCTT analysis in real-time Ethernet networks.

Real-time Ethernet has become a popular solution for handling critical communication in embedded systems, partly thanks to the availability of safe worst-case traversal time analysis. These analyses scale well, but provide pessimistic upper bounds on end-to-end delays leading to over-dimensioning of the network architecture. Computing worst-case delays requires an exhaustive search over all possible scenarios that quickly leads to a combinatorial explosion. Consequently, it is limited to network configuration with less than 100 flows, far from industrial-size ones with more than 1000 flows. In this paper, we propose a hybrid approach (HA) that (1) reduces the number of scenarios to be analysed to get the worst-case delay, (2) leverages exact delays in order to tighten bounds on worst-case delays when the reduced number of scenarios is still too big to be completely analysed. On a realistic avionics case study, HA proved scalable for worst-case delay computations and reduced upper-bound pessimism by over 40%.

Avionics Full-DupleX (AFDX) is a switched Ethernet-based network used in modern commercial airplanes for the transmission of command and control avionics flows. These critical flows require deterministic guarantees leading to a lightly loaded network. Aircraft manufacturers envision to carry additional non avionics flows (i.e. video, audio, service) to take advantage of the spare bandwidth. However, it is then compulsory to preserve the real-time guarantees of avionics flows in terms of bounded jitter at the transmitter output and of bounded end-to-end latency. Depending on the type of additional traffic, Quality of Service (QoS) end-to-end guarantees may be offered to the additional flows of lower criticality in terms of reduced delay or bounded jitter for instance. These guarantees can be ensured by scheduling policies at transmitter and switch level. However, an important safety-related constraint is the asynchronous design of avionics distributed systems that prohibits the use of a network-wide synchronization of end systems and switches. Thus, time-triggered networking such as emerging Time-Triggered Ethernet (TTEthernet) or Time-Sensitive Networking (TSN) cannot be leveraged. This paper underlines the benefits of only scheduling flows at the transmitter, which is compatible with the asynchronous safety constraint of avionics systems. We show that it is possible to build a table schedule that carries both critical avionics flows and additional video flows that meet their timing and bandwidth allocation constraints. Therefore, we design scheduling strategies for efficient distribution of flows in the table scheduling whose performance is compared to the optimal schedule minimizing the emission lag of additional flows. Proposed heuristics are constructed such as to favor the network responsiveness for avionics flows thanks to slot over-provisioning. Extensive results on an A350 AFDX industrial configuration show that for a transmitter load of up to 70% of the available bandwidth, the uniform allocation heuristic provides a performance close to optimal in terms of minimum emission lag for additional flows, so offering a practical configuration heuristic to industry.

Time Sensitive Networking (TSN) is gaining interest in the critical embedded networking community thanks to the various Quality of Service (QoS) mechanisms that can be rolled out to offer different levels of determinism to flows in a switched Ethernet network. Among these standards, limited jitter flows can benefit from the Time Aware Shaper (TAS) which requires the deployment of the IEEE802.1AS synchronization. Indeed, TAS assumes a global time with a bounded drift between any two nodes. In this paper, we derive a refined and general mathematical model that offers upper and lower bounds on the worst-case precision that can be applied to different Ethernet technologies. Results for 100Base-T and 1000Base-T technologies are given. Both simulations and empirical measurements validate the almost two times closer upper bound we obtain compared to the state-of-the-art model.

Deficit Round-Robin (DRR) is a promising service discipline for real-time Ethernet without a global synchronisation. Two improved Network Calculus approaches have been proposed to provide the required bounds on end-to-end delays. The first one is fast but can be optimistic for cornet cases. The second one is safe but highly time consuming. In this paper, we remove the potential optimism of the first approach while keeping its low complexity.

The 28th edition of the Real-Time Networks and Systems Conference (RTNS) was without any doubt very different to previous editions of the conference.The 2020 edition had been planned as an intermediate step in the transition of the conference date from Autumn to Spring.The foreseen venue had been Paris, France.But the travel restriction and the corona pandemic restrictions have put an end to this plan.Instead, RTNS was organized as a purely virtual event.Nevertheless, RTNS 2020 presented 16 papers distributed over four sessions, a session on Real-Time Multicore Systems, on Timing and Monitoring, on Scheduling Systems and on Networked Systems, and a keynote given by Iain Bate from the University of York on "Timing Analysis and Verification of Multi-core Real-Time Systems for Aerospace Applications".Papers recognized as outstanding papers from RTNS 2020 were invited to submit extended journal versions for this special issue of the Real-Time Systems Journal.In total, we invited three submissions that are presented in this issue after rigorous peer review by experts from the areas of real-time and networked systems.Two of the submissions investigate multiprocessor/multicore scheduling, although from fundamentally different perspectives and assumptions, the other paper provides a novel cache analysis which is fundamental to the estimation of worst-case execution time bounds.The first paper in this special issue is "Workload assignment for global real-time scheduling on unrelated multicore platforms" by Antoine Bertout, Joel Goossens, Emmanuel Grolleau and Xavier Poczekajlo.The paper targets task assignment on modern MPSoCs based on a new system model and provides empirical evidence for its practical relevance.The second paper, "Precise and Efficient Analysis of Context-Sensitive Cache Conflict Sets" by Florian Brandner, provides a novel cache and persistence analysis

In a real-time network shared between flows with different criticality, the service discipline in network elements highly impacts the overall performance of the system. Weighted Round Robin (WRR) is a well known simple scheduling policy. It has much lower complexity and cost than Deficit Round Robin (DRR) and exhibits GPS like fairness in a fixed packet size environment.In this paper, we consider WRR in an avionics context where data flows of critical avionic functions must co-exist with noncritical flows in a switched Ethernet network, called AFDX. These flows can have heterogeneous delay constraints and features. Upper bounding the worst-case delays of avionic flows is a mandatory part of the certification process. Meanwhile, sharing AFDX with non-critical flows is envisioned to improve bandwidth utilisation. We show that configuring WRR in such environment is challenging, since frame sizes and deadlines can be very different. We propose a heuristic to distribute critical flows in classes and an exhaustive approach to allocate weights to these classes. Our goal is to achieve maximum bandwidth for noncritical flows while respecting the critical flow deadlines.

AFDX is the de facto communication standard in avionics domain. It is primarily used for the transmission of critical avionic flows. The mandatory certification process requires to upper bound the end-to-end transmission delay for each critical flow. Therefore, worst-case traversal time analysis has been implemented. However, it leads to a very lightly loaded network (up to 10%) as it considers very rare worst-case situations. Introducing a QoS mechanism is often a good solution to improve network utilisation since it allows differentiating critical flows based on their constraints as well as the transmission of less/non-critical flows with bounded impact on critical ones. Deficit Round Robin is such a mechanism and it is envisioned for future avionic networks. Using this mechanism, we propose to share the bandwidth between n - 1 classes for critical flows and one class for non-critical ones. Therefore the contributions of this paper are (1) to propose a quantum assignment that ensures that critical flows always respect their deadlines and maximises the bandwidth for non-critical ones and (2) to propose a heuristic for the distribution of the flows among different classes.

AFDX is the standard switched Ethernet solution for the transmission of avionics flows. Today's AFDX deployments in commercial aircrafts are lightly loaded to ensure the determinism of control and command operations. Manufacturers envision to take advantage of the remaining AFDX bandwidth to transmit additional non avionics flows (video, audio, service). These flows must not compromise the in-time transmission of avionics ones: constraints on jitter at source end system and end-to-end latency have to be insured for each avionics flow. In this paper, we investigate the scheduling of avionics and additional flows, mainly at the end system level. We show that an event-triggered strategy is better than a time-triggered one for additional flows at source level, but it might compromise the jitter constraint of avionics flows and increase the end-to-end latency of additional ones. We consider two time-triggered scheduling strategies, i.e. an optimal one and a simpler one based on a heuristic. We show that the later one performs nearly as well as the former one and that, for both of them, the difference with an event-triggered strategy at source level is limited and can be statically bounded.

Current avionics architecture are based on an avionics full duplex switched Ethernet network (AFDX) that interconnects end systems. Avionics functions exchange data through Virtual Links (VLs), which are static flows with bounded bandwidth. The jitter for each VL at AFDX entrance has to be less than 500μs. This constraint is met, thanks to end system scheduling. The interconnection of many-cores by an AFDX backbone is envisioned for future avionics architecture. The principle is to distribute avionics functions on these many-cores. Many-cores are based on simple cores interconnected by a Network-on-Chip (NoC). The allocation of functions on the available cores as well as the transmission of flows on the NoC has to be performed in such a way that the jitter for each VL at AFDX entrance is still less than 500μs. A first solution has been proposed, where a single task in each many-core manages the transmission of the VLs. This task executes a scheduling table. The access to the Ethernet interface is then only allowed to one VL leading to a significant reduction of the jitter. By oversampling the VL transmissions in a minimum period, the waiting delays are also reduced. But this solution limits the number of VLs. In this paper, we propose to improve the transmission scheduling by relaxing constraint on the over sampling. A new scheduling table is constructed using an Integer Linear Program. This solution increases the number of VLs transmitted by the many-core and still reduces the waiting delays for the transmission of the VLs.

In order to handle mixed criticality flows in a realtime embedded network, switched Ethernet with Quality of Service (QoS) facilities has become a popular solution. Deficit Round Robin (DRR) is such a QoS facility. Worst-Case Traversal Time (WCTT) analysis is mandatory for such systems, in order to ensure that end-to-end delay constraints are met. Network Calculus is a classical approach to achieve this WCTT analysis. A solution has been proposed for switched Ethernet with DRR. It computes pessimistic upper bounds on end-to-end latencies. This pessimism is partly due to the fact that the scheduling of flows by end systems is not considered in the analysis. This scheduling can be modeled by offsets between flows. This modeling has been integrated in WCTT analysis of switched Ethernet with First In First Out (FIFO) scheduling. It leads to a significant reduction of delay upper bounds. The contribution of this paper is to integrate the offsets in the WCTT analysis for switched Ethernet with DRR and to evaluate the reduction on delay upper bounds, considering a realistic case study.

Avionics Full Duplex switched Ethernet (AFDX) is the de facto standard for the transmission of critical avionics flows. It is a specific switched Ethernet solution based on First-in First-out (FIFO) scheduling. Worst-case traversal time (WCTT) analysis is mandatory for such flows, since timing constraints have to be guaranteed. A classical approach in this context is Network Calculus (NC). However, NC introduces some pessimism in the WCTT computation. Moreover, the worst-case often corresponds to very rare scenarios. Thus, the network architecture is most of the time lightly loaded. Typically, less than 10 % of the available bandwidth is used for the transmission of avionics lows on an AFDX network embedded in an aircraft. One solution to improve the utilization of the network is to introduce Quality of Service (QoS) mechanisms. Deficit Round Robin (DRR) is such a mechanism and it is envisioned for future avionics networks. A WCTT analysis has been proposed for DRR. It is based on NC. It doesn't make any assumption on the scheduling of flows by end systems. The first contribution of this paper is to identify sources of pessimism of this approach and to propose an improved solution which removes part of this pessimism. The second contribution is to show how the scheduling of flows can be integrated in this optimized DRR approach, thanks to offsets. An evaluation on a realistic case study shows that both contributions bring significantly tighter bounds on worst-case latencies.

Wireless networks have become a very attractive solution for soft real-time data transport in the industry. For such technologies to carry real-time traffic, reliable bounds on end-to-end communication delays have to be ascertained to warrant a proper system behavior. As for legacy wired embedded and real-time networks, two main wireless multiple access methods can be leveraged: one is time division multiple access (TDMA), which follows a time-triggered paradigm, and the other is carrier sense multiple access with collision avoidance (CSMA/CA), which follows an event-triggered paradigm. This paper proposes an analytical comparison of the time behavior of two representative TDMA and CSMA/CA protocols in terms of the worst-case end-to-end delay. This worst-case delay is expressed in a probabilistic manner because our analytical framework captures the versatility of the wireless medium. Analytical delay bounds are obtained from delay distributions, which are compared to fine-grained simulation results. Exhibited study cases show that TDMA can offer smaller or larger worst-case bounds than CSMA/CA depending on its settings.

Current avionics architectures implemented on large aircraft use complex processors, which are shared by many avionics applications according Integrated Modular Avionics (IMA) concepts. Using less complex processors on smaller aircraft such as helicopters leads to a distributed IMA architecture. Allocation of the avionics applications on a distributed architecture has to deal with two main challenges. A first problem is about the feasibility of a static allocation of partitions on each processing element. The second problem is the worst-case end-to-end communication delay analysis: due to the scheduling of partitions on processing elements which are not synchronized, some allocation schemes are not valid. This paper first presents a mapping algorithm using an integrated approach taking into account these two issues. In a second step, we evaluate, on a realistic helicopter case study, the feasibility of mapping a given application on a variable number of processing elements. Finally, we present a scalability analysis of the proposed mapping algorithm.

In this paper, we consider two Network-on-Chip (NoC) architectures used within commercially available many-core systems, namely Tilera TILE64 which implements flow regulation within routers and KalRay MPPA 256 which implements flow regulation in source nodes. The Worst-Case Traversal Time (WCTT) on the NoC has to be bounded for real-time applications, and buffers should never overflow. Different worst-case analysis approaches have been proposed for each of these NoC architectures. However, no general worst-case analysis supporting both NoC architectures exists in the literature and most approaches are specific to one of the studied NoC. In this paper, we propose to use Recursive Calculus (RC) method for Tilera and KalRay. Furthermore, we compare the performances on a preliminary case study, in terms of WCTT and required buffer capacity. It allows to quantify the trade-off between delays and buffer occupancy.

Wireless networks have become a very attractive solution for soft real-time data transport in the industry. For such technologies to carry real-time traffic, reliable bounds on end-to-end communication delays have to be ascertained to warrant a proper system behavior. As for legacy wired embedded and real-time networks, two main wireless multiple access methods can be leveraged: (i) time division multiple access (TDMA), which follows a time-triggered paradigm and (ii) Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA), which follows an event-triggered paradigm. This paper proposes an analytical comparison of the time behavior of two representative TDMA and CSMA/CA protocols in terms of worst-case end-to-end delay. This worst-case delay is expressed in a probabilistic manner because our analytical framework captures the versatility of the wireless medium. Analytical delay bounds are obtained from delay distributions, which are compared to fine-grained simulation results. Exhibited study cases show that TDMA can offer smaller or larger worst-case bounds than CSMA/CA depending on its settings.

Recent civil airborne platforms are produced using Integrated Modular Avionics (IMA). IMA promotes both sharing of execution and communication resources by the avionics applications. Designs following IMA decrease the weight of avionics equipment and improve the whole system scalability. However, the price to pay for these benefits is an increase of the system's complexity, triggering a challenging system integration process. Central to this integration step are the timing requirements of avionics applications: the system integrator has to find a mapping of applications and communications on the available target architecture (processing modules, networks, etc.) such as end-to-end delay constraints are met. These challenges stress the need for a tool capable of evaluating different integration choices in the early design stages of IMA. In this paper, we present and formalize the problem of spatial and temporal integration of an IMA system. Then, we focus on the temporal allocation problem which is critical to ensure a proper timely behavior of the system. Two main properties are presented to ensure perfect data transmission for hard real-time flows. To quantify the quality of a set of valid temporal allocations, CPM utilization and communication robustness performance criteria are defined. We show on an example that both criteria are antagonist and that they can be leveraged to choose an allocation that either improves the system computing performance or the robustness of the network.

Recent modular avionics architectures have been designed to share computation and communication resources. However, such an approach creates new challenges to master the temporal properties of avionics applications. In the context of IMA (Integrated Modular Avionics), it is crucial to investigate the performance gains that future integration platforms and software will propose. This paper brings to light the impact of spatial and temporal integration choices on the communication performance (e.g. message loss rate, latencies, ...). The conclusion of this investigation is that it is necessary to conduct a thorough modeling and simulation study of an IMA architecture integrating several applications during its early design stages.

The flexibility of wireless connectivity is appealing in the context of industrial networks. This paper discusses the use of a wireless protocol to interconnect remotely located fieldbuses. The focus of this paper is to analyze the feasibility and design issues related to this type of hybrid network architecture. Therefore, we concentrate on deriving appropriate bridging strategies for a network topology composed of remotely located CAN buses interconnected through a wireless local area network following the IEEE802.11g protocol. Using this very simple and cost-effective architecture, we show in this study that by intelligently leveraging the features of CAN and IEEE802.11g in the interconnection policies employed, the missed deadlines can be limited for the CAN frames carried by the wireless network.

Worst case backlog evaluation is a key issue to avoid under or over sizing of output port buffers for store-and-forward switches. Typically, the dimensioning of switches in the context of avionics is at least as important as the upper bounding of the end-to-end delays. This paper presents a new method based on the Trajectory approach for backlog evaluation of output ports of AFDX switches. On an industrial AFDX configuration, this new method leads to an average buffer size reduction of 10% compared to the existing Network Calculus approach.

AFDX (Avionics Full Duplex Switched Ethernet) standardised as ARINC 664 is a major upgrade for avionics systems. Guarantees on worst case end-to-end communication delays are required for certification purposes. These guarantees are obtained thanks to safe upper bounds computed by Network Calculus and trajectory approaches. Indeed, up to now, the computation of an exact worst case delay is intractable for industrial size configurations. An existing approach, based on timed automata, allows the analysis of periodic AFDX configurations with up to 18 flows. This paper proposes a modified timed automata approach which not only increases the size of the configuration for which an exact worst case can be obtained but also supports sporadic flows.

AFDX (Avionics Full Duplex Switched Ethernet) standardized as ARINC 664 is a major upgrade for avionics systems. But network delay analysis is required to evaluate end-to-end delay's upper bounds. The Network Calculus approach, that has been used to evaluate such end-to-end delay upper bounds for certification purposes, is shortly described. The Trajectory approach is an alternative method that can be applied to an AFDX avionics network. We show on an industrial configuration, in which cases the Trajectory approach outperforms the existing end-to-end delays upper bounds and how the combination of the two methods can lead to an improvement of the existing analysis.

AFDX (Avionics Full Duplex Switched Ethernet) standardized as ARINC 664 is a major upgrade for avionics systems. But guarantees on upper bounds of end-to-end communication delays are required for certification purposes. The objective of this paper is to present an improved modeling approach using timed automata for calculation of exact worst case delays. This approach takes advantage of local scheduling of flows. Moreover, it can cope with larger network configurations than existing approaches based on timed automata, thanks to a port by port analysis which reduces the search space.

AFDX (Avionics Full Duplex Switched Ethernet) standardized as ARINC 664 is a major upgrade for avionics systems. The mandatory certification implies a worst-case delay analysis of all the flows transmitted on the AFDX network. Up to now, this analysis is done thanks to a tool based on the Network Calculus approach. This existing approach considers that all the flows transmitted on the network are asynchronous and it does not take into account the scheduling of output flows done by each end system. The main contribution of this paper is to extend the existing Network Calculus approach by introducing the offsets associated to the different periodic flows into the computation. The resulting approach is evaluated on an industrial AFDX configuration with an existing offset assignment algorithm. The obtained upper bounds are significantly reduced.

Avionics Full Duplex Switched Ethernet (AFDX) standardized as ARINC 664 is a major upgrade for avionics systems. The mandatory certification implies a worst-case delay analysis of all the flows transmitted on the AFDX network. Up to now, this analysis is done thanks to a tool based on a Network Calculus approach. The more recent Trajectory approach has been proposed for the computation of worst-case response time in distributed systems. This paper shows how the worst-case delay analysis of the AFDX can be improved using an optimized Trajectory approach. The Network Calculus and the Trajectory approaches are compared on a real avionics AFDX configuration. Moreover, an evaluation of an upper bound of the pessimism of each approach is proposed.

AFDX (avionics full duplex switched Ethernet) standardized as ARINC 664 is a major upgrade for avionics systems. But network delay analysis is required to evaluate end-to-end delay's upper bounds. The network calculus approach, that has been used to evaluate such end-to-end delay upper bounds for certification purposes, is shortly described. In this paper we present how the trajectory approach can be applied to an AFDX avionics network. Moreover we explain how this approach can be optimized in this context. We show that, on an industrial configuration, it outperforms existing end-to-end delays upper bounds.

AFDX (Avionics Full DupleX Switched Ethernet, ARINC 664) developed for the Airbus A380 represents a major upgrade in both bandwidth and capability. Its reliance on Ethernet technology helps to lower some implementation costs, but guaranteed service presents challenges for system designers. An analysis of end-to-end transfer delays through the network is required in order to determine upper bounds. In this paper, we propose to compute probabilistic upper bounds for end-to-end delays on avionic flows. Such upper bounds can be exceeded with a given probability p, and are relevant in the context of avionics, where functions are designed to give accurate results even if they miss some frames. The stochastic network calculus approach analytically determines a probabilistic upper bound, whereas the simulation approach gives an experimental upper bound. The former may be used for new certification needs since it assures that the probability of exceeding the computed upper bound is not greater than p. The latter closely approximates actual network behavior and can help to give some idea of the pessimism of the stochastic network calculus upper bound. The two approaches have been developed in the context of an industrial AFDX network configuration.

AFDX (avionics full duplex switched Ethernet, AR-INC 664) developed for the Airbus A380 represents a major upgrade in both bandwidth and capability. Its reliance on Ethernet technology helps to lower some implementation costs, but guaranteed service presents challenges for system designers. An analysis of end-to-end transfer delays through the network is required in order to determine upper bounds. The stochastic network calculus approach analytically determines worst-case probabilistic upper bounds in the context of homogeneous avionics flows without priorities. Such upper bounds can be exceeded with a given probability PUB, and are relevant in the context of avionics, where functions are designed to give accurate results even if they miss some frames. Nowadays, there is a need to handle new classes of traffics with different priorities (voice, video, best-effort, ...) on the same AFDX network with no consequences on existing avionic flows. This paper presents the application of the stochastic network calculus approach in the context of a static priority queueing service discipline and evaluates the influence of the service discipline on analytical probabilistic upper bounds.

AFDX (Avionics Full Duplex Switched Ethernet, ARINC 664) used for modern aircraft such as Airbus A380 represents a major upgrade in both bandwidth and capability for aircraft data networks. Its reliance on Ethernet technology helps to lower some of the implementation costs, though the requirement for guaranteed service does present challenges to system designers. Thus, the problem is to prove that no frame will be lost by the network (no switch queue will overflow) and to evaluate the end-to-end transfer delay through the network. Several approaches have been proposed for this evaluation. Network calculus gives a guaranteed upper bound on end-to-end delays, while simulation produces more accurate results on a given set of scenarios. Main problem of simulation is to find a representative subset among the huge number of possible scenarios. In this paper, we propose an original and promising approach to drastically reduce the number of possible scenarios. We illustrate this approach on a realistic industrial network configuration.

Architectures of avionics networks, such as that of the Airbus A380, currently know important evolutions. This is principally due to the increase in the complexity of the embedded systems, in term of rise in number of integrated functions and their connectivity. The evolution of switched Ethernet technologies allows their implementation as an avionics architecture (AFDX: avionics full duplex switched Ethernet). The problem is then to prove that no frame is lost by the network (no switch queue will overflow) and to evaluate the end-to-end transfer delay through the network. The objective of this paper is to present and shortly compare three methods for the evaluation of end-to-end delays: network calculus, queuing networks simulation and model checking

Embedded systems have specific real-time requirements that led to the development of dedicated communication protocols. Such systems often face increasing communication needs and the integration of switched Ethernet architecture. But moving from existing dedicated field-buses architectures to new Ethernet based architectures is not always easily feasible, due to industrial constraints. In this paper, we propose a solution for integrating existing data busses (such as CAN, which is an important standard in automotive context) on a global architecture that respects increasing bandwidth requirements. We consider a time triggered CAN application and propose CAN/Ethernet bridging strategies that respect the time-triggered real time behaviour of CAN End System when communicating through a switched Ethernet network that can also be shared by (non CAN) applications

The Grafcet (or sequential function charts) language is a graphic language often offered in programmable logic control systems (PLC) used for industrial control-command applications. Modeling of Grafcet by the synchronous data-flow language Signal gives both explicit semantics, and the corresponding simulator. The translation into a graph of tasks makes it possible to execute the Grafcet program on any hardware architecture. Moreover, the use of Signal's proof tools allows verification of Grafcet properties, opening the field of critical applications to this very expressive language.