We study the existence of infinite and safe schedules for resource-dependent real-time systems, in the setting of multiple continuous resources. Specifically, we explore the multi-variable extension of Energy Timed Automata, where variables are bounded by polyhedra in . We ask the question of whether there exist infinite runs satisfying such boundary constraints and show how schedules can be synthesized by characterising these runs as limit sets using quantifier elimination for linear real arithmetic. We show that for linear limit sets, it is possible to characterise such infinite runs. Additionally, we relate this to an earlier decidability result for single-variable Energy Timed Automata that are flat and segmented, and show constructively that there exist flat and segmented multi-variable Energy Timed Automata that give rise to non-linear limit sets. Lastly, we solidify our framework and method with a case study. Specifically, a multi-agent extension of an industrial case concerned with oil tanks, originally provided by the HYDAC company.

The existing worst-case response time (WCRT) analysis for individual priority classes under credit-based shaping (CBS) in Ethernet AVB based on so-called eligible intervals is both independent and tight. This WCRT analysis does not rely on any assumptions on interfering inter-priority streams other than those enforced by the Ethernet standard. A major advantage of this independent analysis is that CBS may be viewed as resource reservation, where allocated bandwidth is both guaranteed and enforced. Although independent analysis provides inter-priority class robustness, it comes at a cost of over-provisioning bandwidth. We illustrate this cost of inter-priority class robustness by means of an example that requires 7.8 times the amount of bandwidth reservation for a given set of streams compared to a different analysis that takes knowledge of inter-priority streams into account.

To meet their stringent requirements in terms of performance and dependability, communication networks should be "well connected". While classic connectivity measures typically revolve around topological properties, e.g., related to cuts, these measures may not reflect well the degree to which a network is actually dependable. We introduce a more refined measure for network connectivity, the hazard value, which is developed to meet the needs of a real network operator. It accounts for crucial aspects affecting the dependability experienced in practice, including actual traffic patterns, distribution of failure probabilities, routing constraints, and alternatives for services with preferences therein. We analytically show that the hazard value fulfills several fundamental desirable properties that make it suitable for comparing different network topologies with one another, and for reasoning about how to efficiently enhance the robustness of a given network. We also present an optimised algorithm to compute the hazard value and an experimental evaluation against networks from the Internet Topology Zoo and classical datacenter topologies, such as fat trees and BCubes. This evaluation shows that the algorithm computes the hazard value within minutes for realistic networks, making it practically usable for network designers.

Complex embedded systems, such as robotics, automotive and high-tech manufacturing, are hard to maintain due to their complex nature. To advance our understanding of the software engineering practice for complex embedded systems, we conducted a series of empirical studies at ASML, a leading manufacturer of lithography machines for semi-conductor industry. We started with an interview study exploring how developers use execution logs, essential artifacts that capture the runtime behavior of software systems. The empirical insights obtained from this study led us to explore subtopics about model inference from logs, modeling practice and log comparison. Motivated by the observation that developers often manually sketch behavioral models based on logs, we propose a model inference technique that can extract models by combining log analysis, and analysis of a running system under stimuli. As observed in this model inference study, the transition from code to models requires developers to work with a hybrid system which consists of handwritten code and models. We then study modeling practices and the roles of model in such hybrid systems. Particularly, we study why developers violate modeling guidelines, providing implications for researchers and tool builders to support developers in modeling complex embedded systems. Another interesting observation from the interview study is that developers face challenges in comparing multiple logs generated from such systems. We therefore conduct a literature study to provide an overview of the existing techniques and identify the limitations of the existing techniques. In this project, we study logs and models in complex embedded systems, providing tool builders, researchers and practitioners with implications to facilitate log analysis, model inference, modeling practice and log comparison.

Abstract Context Models, as the main artifact in model-driven engineering, have been extensively used in the area of embedded systems for code generation and verification. One of the most popular behavioral modeling techniques is the state machine. Many state machine modeling guidelines recommend that a state machine should have more than one state in order to be meaningful. However, single-state state machines (SSSMs) violating this recommendation have been used in modeling cases reported in the literature. Objective We aim for understanding the phenomenon of using SSSMs in practice as understanding why developers violate the modeling guidelines is the first step towards improvement of modeling tools and practice. Method To study the phenomenon, we conducted an exploratory study which consists of two complementary studies. The first study investigated the prevalence and role of SSSMs in the domain of embedded systems, as well as the reasons why developers use them and their perceived advantages and disadvantages. We employed the sequential explanatory strategy, including repository mining and interview, to study 1500 state machines from 26 components at ASML, a leading company in manufacturing lithography machines from the semiconductor industry. In the second study, we investigated the evolutionary aspects of SSSMs, exploring when SSSMs are introduced to the systems and how developers modify them by mining the largest state-machine-based component from the company. Results We observe that 25 out of 26 components contain SSSMs. Our interviews suggest that SSSMs are used to interface with the existing code, to deal with tool limitations, to facilitate maintenance and to ease verification. Our study on the evolutionary aspects of SSSMs reveals that the need for SSSMs to deal with tool limitations grew continuously over the years. Moreover, only a minority of SSSMs have been changed between SSSM and multiple-state state machine (MSSM) during their evolution. The most frequent modifications developers made to SSSMs is inserting events with constraints on the execution of the events. Conclusions Based on our results, we provide implications for developers and tool builders. Furthermore, we formulate hypotheses about the effectiveness of SSSMs, the impacts of SSSMs on development, maintenance and verification as well as the evolution of SSSMs.

Models, as the main artifact in model-driven engineering, have been extensively used in the area of embedded systems for code generation and verification. One of the most popular behavioral modeling techniques is state machine. Many state machine modeling guidelines recommend that a state machine should have more than one state in order to be meaningful. However, single-state state machines (SSSMs) violating this recommendation have been used in modeling cases reported in the literature.

Flow control is of particular importance in TimeSensitive Networking (TSN), where timeliness of messages is guaranteed through several types of traffic shaping. This has given rise to a number of papers discussing the worst-case response time analysis of, in particular, the credit-based traffic shaping approach. In this work-in-progress paper, we concern ourselves with the possibility that traffic shaping can be applied in different layers of the protocol stack, e.g., the physical layer and link layer, which may give rise to different credit behaviors. We convey our concern that the analysis performed in literature seems to assume application of traffic shaping in the physical layer, and that the analysis therefore cannot be readily used in a context where shaping is applied in a higher layer. In particular, assuming application of credit-based shaping in the link layer, there are different interpretations possible for credit behavior. Depending on the interpretation, some of the basic properties of credit, that are crucial for the analysis, may no longer be valid after overhead is added by the physical layer. As an ongoing effort, we plan to revisit the eligible interval analysis of [1] with an adaptation for a link layer interpretation of the standard concerning application of traffic shaping.

In the high-tech and automotive industry, bandwidth considerations and widely accepted standardization are two important reasons why Ethernet is currently being considered as an alternative solution for real-time communication (compared to traditional fieldbusses). Although Ethernet was originally not intended for this purpose, the development of the Ethernet AVB standard enables its use for transporting high-volume data (e.g. from cameras and entertainment applications) with low-latency guarantees. In complex industrial systems, the network is shared by many applications, developed by different parties. To face this complexity, the development of these applications must be kept as independent as possible. In particular, from a network point of view, progress of all communication streams must be guaranteed, and the performance for individual streams should be predictable using only information regarding the stream under study and the general parameters of the communication standard used by the network. Initial methods to guarantee latency for Ethernet AVB networks rely on the traditional busy-period analysis. Typically, these methods are based on knowledge of the inter-arrival patterns of both the stream under study and the interfering streams that also traverse the network. The desired independence is therefore not achieved. In this paper, we present an independent real-time analysis based on so-called eligible intervals , which does not rely on any assumptions on interfering priority classes other than those enforced in the Ethernet AVB standard. We prove this analysis is tight in case there is only a single higher-priority stream, and no additional information on interference is known. In case there are multiple higher-priority streams, we give conditions under which the analysis is still tight. Furthermore, we compare the results of our approach to the two most recent busy-period analyses, point out sources of pessimism in these earlier works, and argue that assuming more information on the sources of interference (e.g. a minimal inter-arrival time between interfering frames) has only limited advantages.

In the automotive industry, Ethernet is currently being introduced as a viable solution for real-time communication with high bandwidth requirements. In this paper, we present and prove a tight bound for the relative best-case response time of a frame in an Ethernet AVB switch compared to its response time in a schedule without interference. Our analysis is based on the observation that frames in a burst, scheduled using a credit shaping policy, may be scheduled earlier in case of interference than in a schedule without interference. We show how an upper bound on the build up of credit may be used to bound this relative speed-up of frames.

Busy period analysis is often used as a basis for worst-case response time analysis of priority based systems. However, when shaping strategies are used to prevent starvation of lower priorities, it becomes difficult to achieve tightness results using this method. The reason for this is that a busy period is defined as the longest interval in which there exists pending load. It is exclusively based on execution time, and does not take the amount of provided bandwidth into account. As a consequence, it is less suitable for the study of idling systems. In particular, we do not yet have tightness results regarding the analysis of the Ethernet AVB standard, in which credit-based shaping is applied. In this paper, we propose an alternative to the use of busy periods. We show that, by defining an eligible interval in such a way that provisioning is taken into account, tight worst-case response time bounds can more easily be obtained for Ethernet AVB, at least in the case of either lower-or higher-priority interference.

We present a solution for service discovery of resource constrained devices based on mDNS/DNS-SD. We extend the mDNS/DNS-SD service discovery protocol with support for proxy servers. Proxy servers temporarily store information about services offered on resource constrained devices and respond on their behalf while they are not available. We analyze two protocols for the delegation mechanism between a service provider and a proxy server: an active proxy protocol, as used in the mDNS/DNS-SD implementation by Apple, and a new, passive proxy protocol. We implement and simulate both approaches. Based on the delay and energy usage, we show that the second approach converges faster, thus saving more energy by allowing the resource constrained device to be turned off earlier.

This paper proposes a new data ow model for analyzing the worst-case temporal behavior of resource arbitration through Time Division Multiplexing (TDM).

HyPA is an algebraic theory based on the classical process algebra Algebra of Communicating Processes (ACP) for the specification and analysis of hybrid systems. We have the idea that HyPA is also well suited for addressing various aspects of digital embedded systems including hardware, software and concurrency, as well as mixed-signal designs. To show that HyPA is useful for the specification and analysis of hybrid systems and that our idea is correct, we illustrate the use of HyPA with some case studies: a point-to-point communication , a thermostat, a positive-edge-triggered D flip flop, and a small part of a mixed-signal fuzzy controller.