Abstract This paper analyzes the timing performance of a persistent storage designed for distributed container-based architectures in industrial control applications. The timing performance analysis is conducted using an in-house simulator, which mirrors our testbed specifications. The storage ensures data availability and consistency even in presence of faults. The analysis considers four aspects: 1. placement strategy, 2. design options, 3. data size, and 4. evaluation under faulty conditions. Experimental results considering the timing constraints in industrial applications indicate that the storage solution can meet critical deadlines, particularly under specific failure patterns. Comparison results also reveal that, while the method may underperform current centralized solutions in fault-free conditions, it outperforms the centralized solutions in failure scenario. Moreover, the used evaluation method is applicable for assessing other container-based critical applications with timing constraints that require persistent storage.

In this paper, we analyze the scalability and performance of a persistent, fault-tolerant storage approach that provides data availability and consistency in a distributed container-based architecture with intended use in industrial control applications. We use simulation to evaluate the performance of this storage system in terms of scalability and failures. As the industrial applications considered have timing constraints, the simulation results show that for certain failure patterns, it is possible to determine whether the storage solution can meet critical deadlines. The presented approach is applicable for evaluating timing constraints also of other container-based critical applications that require persistent storage.

Switched networks following the time-triggered paradigm rely on static schedules that determine the communication pattern over each link. In order to tolerate link failures, methods based on spatial redundancy and based on resynthesis and replacement of schedules have been proposed. These methods, however, do not scale to larger networks, which may be needed e.g. for future large-scale cyberphysical systems. We propose a distributed Self-Healing Protocol (SHP) that, instead of recomputing the whole schedule, repairs the existent schedule at runtime. For that, it relies on the coordination among the nodes of the network to redefine the repair problem as a number of local synthesis problems of significantly smaller size, which are solved in parallel by the nodes that need to reroute the frames affected by link failures. SHP exhibits a high success rate compared to full rescheduling, as well as remarkable scalability; it repairs the schedule in milliseconds, whereas rescheduling may require minutes for large networks.

In our previous work we proposed a fault-tolerant persistent storage for container-based fog architecture. We leveraged the use of containerization to provide storage as a containerized application working along with other containers. As a fault-tolerance mechanism we introduced a replicated data structure and to solve consistency issue between the replicas distributed in the cluster of nodes, we used the RAFT consensus protocol. In this paper, we verify our proposed solution using the UPPAAL model checker. We explain how our solution is modeled in UPPAAL and present a formal verification of key properties related to persistent storage and data consistency between nodes.

The Time-Triggered paradigm presents a lack of flexibility due to the required static scheduled. If an unpredicted event occurs, a new schedule needs to be synthesized. Centralized approaches have been proposed to obtain such schedules during runtime, while fully-distributed approaches seek to repair only the affected sections of the schedule. This paper proposes a Semi-Distributed Self-Healing Protocol that pursues to combine the benefits of both approaches. We study the applicability of our protocol repairing schedules after link failures. Early results show that link failures can be repaired in 2ms for the evaluated network.

Fog computing has been recently introduced to bridge the gap between cloud resources and the network edge. Fog enables low latency and location awareness, which is considered instrumental for the realization of IoT, but also faces reliability and dependability issues due to node mobility and resource constraints. This paper focuses on the latter, and surveys the state of the art concerning dependability and fog computing, by means of a systematic literature review. Our findings show the growing interest in the topic but the relative immaturity of the technology, without any leading research group. Two problems have attracted special interest: guaranteeing reliable data storage/collection in systems with unreliable and untrusted nodes, and guaranteeing efficient task allocation in the presence of varying computing load. Redundancy-based techniques, both static and dynamic, dominate the architectures of such systems. Reliability, availability and QoS are the most important dependability requirements for fog, whereas aspects such as safety and security, and their important interplay, have not been investigated in depth.

Software-to-hardware allocation plays an important role in the development of resource-constrained automotive embedded systems that are required to meet timing, reliability and power requirements. This paper proposes an Integer Linear Programming optimization approach for the allocation of fault-tolerant embedded software applications that are developed using the AUTOSAR standard. The allocation takes into account the timing and reliability requirements of the multirate software applications and the heterogeneity of their execution platforms. The optimization objective is to minimize the total power consumption of the applications that are distributed over multiple computing units. The proposed approach is evaluated using a range of different software applications from the automotive domain, which are generated using the real-world automotive benchmark. The evaluation results indicate that our proposed allocation approach is effective while meeting the timing, reliability, and power requirements of the considered automotive software applications.

The use of lightweight formal methods (LFM) for the development of industrial applications has become a major trend. Although the term "lightweight formal methods" has been used for over ten years now, there seems to be no common agreement on what "lightweight" actually means, and different communities apply the term in all kinds of ways. In this paper, we explore the recent trends in the use of LFM, and establish our opinion that cost-effectiveness is the driving force to deploy LFM. Further, we propose a simple framework that should help to classify different LFM approaches and to estimate which of them are most cost-effective for a certain software engineering project. We demonstrate our framework using some examples.

Time-Triggered communication is based on generating an offline static schedule that guarantees frame transmissions with reduced latency and low jitter. However, static schedules are not adaptive: if some unpredicted event happens, like a link failure, the schedule is not valid anymore and a new one needs to be synthesized from scratch. This paper presents a novel hot-patching protocol which seeks, after a link failure disconnecting two nodes, to find a new path to reconnect both nodes and restore during run-time the affected part of the schedule. We also introduce the concept of reparability as a desired property of the schedule, which increases the probability of our protocol to succeed. The first evaluation shows that our hot-patching protocol can recover from a link failure consistently in less than 25ms.

The time-triggered communication paradigm has been shown to satisfy temporal isolation while providing end to end delay guarantees through the synthesis of an offline schedule. However, this paradigm has severe flexibility limitations as any unpredicted change not anticipated by the schedule, such as a component failure, might result in a loss of frames. A typical solution is to use redundancy or replace and update the schedule offline anew. With the ever increase in size of networks and the need to reduce costs, supplementary solutions that enhance the reliability of such networks are also desired. In this paper, we introduce a repair algorithm capable of reacting to unpredicted link failures. The algorithm quickly modifies the schedule such that all frames are transmitted again within their timing guarantees. We found that the success of our algorithm increases significantly with the existence of empty slots spread over the schedule, an opposite approach compared to packing frames, commonly used in the literature. We propose a new ILP formulation that includes a maximization of frame and link intermissions to stretch empty slots over the schedule. Our results show that we can repair with 90% success rate within milliseconds to a valid schedule compared to a few minutes needed to re-schedule the whole network.

Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a (κ, ℓ)-resistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least ℓ, no matter what sequence of at most κ links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a (κ, ℓ)-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is (κ, ℓ)-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not (κ, ℓ)-resistant. We illustrate the applicability of our approach using an SMT-based implementation.

In this paper we address particular aspects of integration of formal methods in large-scale industrial projects, namely collaborative aspects. We review recent works addressing such aspects, identify some current trends and discuss directions for further research.

Ethernet-based networks have found their way into industrial communication more than a decade ago. However, while industry and academia developed Ethernet variants to also meet real-time and fault-tolerant requirements, recent standardization efforts within the IEEE 802 will broadly bring standard IT switched Ethernet in future industrial communication networks. As first standards of IEEE 802.1 time-sensitive networking (TSN) are becoming published at the time of this writing, we review these standards and formulate further research challenges that still go beyond current standard developments. Furthermore, we report on recent research results from the RetNet project that target these research challenges.

Time-triggered offline scheduling is a cost-efficient way to guarantee low communication end-to-end latency and minimal jitter for communication networks in real-time systems. The schedule is generated pre-runtime and indicates the transmission times of time-triggered frames such that contention is prevented. The synthesis of such offline schedules is a bin-packing problem, known to be NP-complete, with complexity driven by the constraints on frame transmissions, and the number of frames in the schedule. Satisfiability Modulo Theories combined with segmented approaches have been successfully used for synthesizing schedules of large networks. However, such synthesis did not take into account frames periods that are much shorter than the time to execute the schedule cycle. This paper presents a period-aware segmented approach that takes into account the frame periods in order to allocate various instances of a frame within a single cycle. We describe three different synthesis strategies and evaluate them with different synthetic experiments. The results show better performance for one of the strategies, which can synthesize schedules of large networks with high communication loads in less than one hour. We also report how the synthesis time and the schedule quality can change with different parameter configurations.

Real-time networks have tight communication latency and minimal jitter requirements. One way to ensure these requirements is the implementation of a static schedule, which defines the transmission points in time of time-triggered frames. Synthesizing such static schedules is known to be an NP-complete problem where the complexity is driven by the large number of constraints imposed by the network. Satisfiabily Modulo Theories (SMT) have been proven powerful tools to synthesize schedules of medium-to-large industrial networks. However, the schedules of new extremely large networks, such as integrated multi-machine factory networks, are defined by an extremely large number of constraints exceeding the capabilities of being synthesized by the tool alone. This paper presents a decomposition approach that will allow us to improve to synthesize schedules with up to two orders of magnitude in terms of the number of constraints that can be handled. We also present an implementation of a dependency tree on top of the decomposition approach to address application-imposed constraints between frames.

ISO 26262 is the new standard for automotive functional safety. This standard identifies major process steps across a large number of system stages as well as safety-related artifacts required as input and output of these steps. The VeriSpec project intends to identify the main challenges for the adoption of ISO 26262 by the heavy-vehicle industry and to provide useful and industrially relevant "components" (methods, tools etc.) required by the standard. The project work targets two main research goals: (i) requirement formalization support, including a usable front-end for specifying requirements by using patterns, and (ii) formal analysis of realizations in form of architectural models at various levels of abstraction, by model-checking the formal representations of the latter. In this paper, we present the current challenges facing industry and justifying VeriSpec, together with a preliminary roadmap for the research.

For a distributed embedded system (DES) to operate continuously in a dynamic environment, it must be flexible and highly reliable. This applies in particular to its communication subsystem. The Flexible Time-Triggered Replicated Star for Ethernet (FTTRS) aims at providing such a subsystem by means of a highly-reliable switched-Ethernet architecture based on the Flexible Time-Triggered paradigm (FTT), a master/slave communication paradigm where the master periodically polls the slaves using so-called trigger messages (TMs). In particular, FTTRS interconnects nodes by redundant communication paths provided by two switches, each embedding an FTT master that manages the communication. This allows FTTRS to tolerate the failure of one switch without interrupting the communication as long as the masters are replica determinate, i.e., provide identical service to the slaves. The master replica determinism entails the masters broadcasting their TMs in a lockstep fashion: when one master broadcasts a TM, the other should do the same quasi-simultaneously. In this paper we present a solution inspired by the Precision Time Protocol (PTP) for achieving this lockstep transmission and preliminary results showing the precision with which we can synchronize the masters on a software prototype.

The importance of using formal methods and techniques for verification of requirements in the automotive industry has been greatly emphasized with the introduction of the new ISO26262 standard for road vehicles functional safety. The lack of support for formal modeling of requirements still represents an obstacle for the adoption of the formal methods in industry. This paper presents a case study that has been conducted in order to evaluate the difficulties inherent to the process of transforming the system requirements from their traditional written form into semi-formal notation. The case study focuses on a set of non-structured functional requirements for the Electrical and Electronic (E/E) systems inside heavy road vehicles, written in natural language, and reassesses the applicability of the extended Specification Pattern System (SPS) represented in a restricted English grammar. Correlating this experience with former studies, we observe that, as previously claimed, the concept of patterns is likely to be generally applicable for the automotive domain. Additionally, we have identified some potential difficulties in the transformation process, which were not reported by the previous studies and will be used as a basis for further research.

The interest to use Switched Ethernet technologies in real-time communication is increasing due to its absence of collisions when transmitting messages. Nevertheless, using COTS switches affect the timeliness guarantee inherent in potentially overflowing internal FIFO queues. In this paper we focus on a solution, called the FTT-SE protocol, which is developed based on a master-slave technique. Recently, an extension of the FTT-SE protocol has been proposed where the transmission of messages are controlled using multiple master nodes. In order to guarantee the correctness of the protocol, the masters should be timely synchronized. Therefore, in this paper we investigate the possibility of using a clock synchronization protocol, based on the IEEE 1588 standard, among master nodes. Moreover, we evaluate the overhead that is imposed by the clock synchronization protocol to the FTT-SE protocol. Finally, we present a formal verification of this solution by means of model checking technique to prove the correctness of the FTT-SE protocol when the clock synchronization protocol is applied.

Hard Real-Time Ethernet Switching (HaRTES) is an implementation of the Flexible Time Triggered (FTT) communication paradigm over Switched Ethernet, which intends to provide hard real-time communication in a flexible manner. This paper presents a first proposal for enhancing HaRTES with a service of total order multicast for synchronous messages. This service uses the centralized online scheduling service of FTT in order to reduce complexity and bandwidth utilization.

The application of model checking for the formal verification of distributed embedded systems requires the adoption of techniques for realistically modeling the temporal behavior of such systems. This paper discusses how to model with timed automata the different types of relationships that may be found among the computer clocks of a distributed system, namely, ideal clocks, drifting clocks, and synchronized clocks. For each kind of relationship, a suitable modeling pattern is thoroughly described and formally verified.

Despite the significant advantages of the Controller Area Network (CAN) there is an extended belief that CAN is not suitable for critical applications, mainly because of several dependability limitations. During the CANbids project each one of these limitations has been addressed and a complete architecture for CAN-based fault-tolerant systems has been devised. This architecture allows building highly-reliable systems. This paper describes the design of such an architecture and the prototyping of its fundamental parts.

There is a growing interest in making the CAN field-bus more suitable for dependable applications. In the past years, several dependability limitations of CAN have already been addressed and a significant number of solutions are available. Nevertheless, the integration of these solutions into a single communication infrastructure is still an open issue. In this paper we discuss the integration of two specific solutions: FTT-CAN and ReCANcentrate. FTT-CAN is a higher-layer protocol that guarantees flexible real-time scheduling of CAN messages; whereas ReCANcentrate is a duplicated star topology for CAN that includes several enhanced mechanisms for media fault tolerance. We show how they are integrated into a single architecture that preserves the properties of each solution.

Although the specification of CAN states that this protocol provides data consistency, it is well know that said property does not hold for certain specific error scenarios affecting the last bits of a CAN frame, and a number of solutions have been already suggested. Morever, for a long time it has been thought that the errors affecting the initial or intermediate bits of a CAN frame cannot cause any inconsistency. In this paper we show that this assumption is false, and that such kinds of message inconsistencies are also possible for certain combinations of multiple channel errors. After describing these unreported scenarios of inconsistency, we present a mechanism that guarantees the consistent detection of said scenarios and elimininates the possibility of suffering this kind of inconsistencies. This mechanism is therefore useful for the design of highly-dependable applications over CAN.

The main goal of a clock synchronization service is to keep a consistent perception of time among the nodes of the system. In this context, consistency means that at any instant, the values of all the clocks in the system do not differ more than a given amount, which is called the precision. Moreover, clock synchronization is said to be fault tolerant if the intended precision is guaranteed despite the occurrence of the faults included in the fault model. In this paper, we consider a specific fault-tolerant master/slave clock synchronization service for the Controller Area Network (CAN) field bus, and analyze its precision under different fault assumptions. The equations obtained in our analysis show that, when using master redundancy, inconsistent channel faults may have a negative impact on the guaranteed precision.

The controller area network (CAN) is facing a great opportunity. The maturity of this technology makes many researchers believe that CAN may be adopted in more critical systems. However, the suitability of CAN for these challenging applications strongly depends on our capacity to integrate all the solutions already available into a single, comprehensive architecture. We claim that clock synchronization plays a fundamental role in such architecture. Therefore, the means to achieve a solution fulfilling the expected requirements on reliability, cost, and precision must be deeply investigated. This paper discusses the relevance of clock synchronization in the future of CAN systems and describes a novel solution to supply this service. This solution exhibits several advantages: it provides very high precision, causes very low communication and computation overhead, and includes mechanisms to provide fault tolerance. Moreover, and in contrast to previous proposals, it is designed to be orthogonal to the rest of the system. Thus, it can be directly incorporated to any CAN system, without having to replace any of the components, which reduces the cost increment caused by the new service.

The controller area network (CAN) is a field bus that is nowadays widespread in distributed embedded systems due to its electrical robustness, low price, and deterministic access delay. However, its use in safety-critical applications has been controversial due to dependability limitations, such as those arising from its bus topology. In particular, in a CAN bus, there are multiple components such that if any of them is faulty, a general failure of the communication system may happen. In this paper, we propose a design for an active star topology called CANcentrate. Our design solves the limitations indicated above by means of an active hub, which prevents error propagation from any of its ports to the others. Due to the specific characteristics of this hub, CANcentrate is fully compatible with existing CAN controllers. This paper compares bus and star topologies, analyzes related work, describes the CANcentrate basics, paying special attention to the mechanisms used for detecting faulty ports, and finally describes the implementation and test of a CANcentrate prototype.

The traditional approaches to the design of distributed safety-critical systems, due to fault-tolerance reasons, have mostly considered static cyclic table-based traffic scheduling. However, there is a growing demand for operational flexibility and integration, mainly to improve efficiency in the use of system resources, with the network playing a central role to support such properties. This calls for dynamic online traffic scheduling techniques so that dynamic communication requirements are adequately supported. Nevertheless, using dynamic traffic management mechanisms raises additional problems, in terms of fault-tolerance, related with the weaker knowledge of the future system state caused by the higher level of operational flexibility. Such problems have been recently addressed in the scope of using flexible time-triggered CAN (FTT-CAN) in safety-critical applications in order to benefit from the high operational flexibility of this protocol. This paper gathers and reviews the main mechanisms that were developed to provide dependability to the protocol, namely, master replication and fail-silence enforcement.

This work-in-progress (WIP) paper presents server-CAN and highlights its operation and possible vulnerabilities from a fault tolerance point of view. The paper extends earlier work on server-CAN by investigating the behaviour of server-CAN in faulty conditions. Different types of faults are described, and their impact on sever-CAN is discussed, which is the subject of on-going research

Advances in programmable hardware have simplified integration of communication facilities in low-cost hardware components. This has proved to be beneficial in the design of distributed embedded systems as it allows the communication subsystem to provide important properties at a low level. The present work follows this approach in order to achieve timeliness in CAN networks. This paper describes the implementation of the LST-CAN protocol in programmable hardware. This protocol is an extension to CAN which ensures timely communication regardless of environmental interferences.

It has been reported that some particular fault scenarios may cause malfunction of the controller area network protocol. Although such scenarios are very unlikely, they become relevant when attempting to use the CAN protocol for critical applications. The fault injector described in this paper induces these fault scenarios at the physical layer of the CAN protocol by means of a software tool and a set of specifically designed circuits. Therefore, and in contrast to previous solutions, this fault injector is suitable to evaluate most of the dependability mechanisms that have been proposed for CAN networks.

As CANs (controller area networks) are being increasingly used in safety-critical applications, there is a need for accurate predictions of failure probability. In this paper we provide a general probabilistic schedulability analysis technique which is applied specifically to CANs to determine the effect of random network faults on the response times of messages. The resultant probability distribution of response times can be used to provide probabilistic guarantees of real-time behaviour in the presence of faults. The analysis is designed to have as little pessimism as possible but never be optimistic. Through simulations, this is shown to be the case. It is easy to apply and can provide useful evidence for justification of an event-triggered bus in a critical system.