Component-based and model-based reasonings are key concepts to address the increasing complexity of real-time systems. Bounding abstraction theories allow to create efficiently analyzable models that can be used to give temporal or functional guarantees on non-deterministic and non-monotone implementations. Likewise, bounding refinement theories allow to create implementations that adhere to temporal or functional properties of specification models. For systems in which jitter plays a major role, both best-case and worst-case bounding models are needed. In this paper we present a bounding abstraction-refinement theory for real-time systems. Compared to the state-of-the-art TETB refinement theory, our theory is less restrictive with respect to the automatic lifting of properties from component to graph level and does not only support temporal worst-case refinement, but evenhandedly temporal and functional, best-case and worst-case abstraction and refinement.
A commonly used approach to develop parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to prove correctness of compiler directives combined with functional correctness of the program. We propose syntax and semantics for a simple core language, capturing the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorized and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show that it is sufficient to have contracts for the basic blocks to prove correctness of the compiler directives, and moreover that functional correctness of the sequential program implies correctness of the parallelized program. We formally prove correctness of our approach. In addition, we define a widely-used subset of OpenMP that can be encoded into our core language, thus effectively enabling the verification of OpenMP compiler directives, and we discuss automated tool support for this verification process.
As part of our co-operation with the Telecommunication Agency of the Netherlands, we want to formulate an accident analysis method and model for use in incidents in telecommunications that cause service unavailability. In order to not re-invent the wheel, we wanted to first get an overview of all existing accident analysis methods and models to see if we could find an overarching method and commonalities between models. Furthermore, we wanted to find any methods that had been applied to incidents in telecommunication networks or even been designed specifically for these incidents. In this article, we present a systematic literature review of incident and accident analysis methods across domains. We find that accident analysis methods have experienced a rise in attention over the last 15 years, leading to a plethora of methods. We discuss the three classes in which they are often categorized. We find that each class has its own advantages and disadvantages: an analysis using a sequential method may be easier to understand and communicate and quicker to execute, but may miss vital underlying causes that can later trigger new, similar accidents. An analysis using an epidemiological method takes more time, but it also finds underlying causes the resolution of which may prevent accidents from happening in the future. Systemic methods are appropriate for complex, tightly coupled systems and executing such a method takes a lot of time and resources, rendering it very expensive. This will often not be justified by the costs of the accident (especially in telecommunications networks) and it will therefore be too expensive to be employed in regular businesses. We were not able to find any published definitions of structured methods specific to telecommunications, nor did we find any applications of structured methods specifically to telecommunications.
Although there have been many attempts to define the concept ‘computer literacy’, no consensus has been reached: many variations of the concept exist within litera-ture. The majority of papers does not explicitly define the concept at all, insteadusing an unjustified subset of elements related to computers to assess a subject’slevel of computer literacy. This can limit the generalizability of research and canlead to fallacious conclusions. This is an internal report listing the method by whichthe research was conducted.
Mobile remote presence systems (MRPs) are the logical next step in telepresence, but what are the ethical, social, legal, and technical implications of such systems going into the wide wild world? We explored these potential issues by immersing ourselves in a range of possible applications by re-purposing commercially available MRPs. This researcher-as-experimental-subject (RAES) approach allowed us to quickly identify many possible issues that could arise from use of the technology. Considering such issues can help further the use of telepresence robots in real-life settings. Furthermore, we suggest that the RAES approach could be helpful in finding interesting issues that might arise when new technologies are introduced to the consumer market.
Real-time streaming applications with cyclic data dependencies that are executed on multiprocessor systems with processor sharing usually require a temporal analysis to give guarantees on their temporal behavior at design time. Current accurate analysis techniques for cyclic applications that are scheduled with Static Priority Preemptive (SPP) schedulers are however limited to the analysis of applications that can be expressed with Homogeneous Synchronous Dataflow (HSDF) models, i.e. in which all tasks operate at a single rate. Moreover, it is required that both input and output buffers synchronize atomically at the beginnings and finishes of task executions, which is difficult to realize on many existing hardware platforms. This paper presents a temporal analysis approach for cyclic real-time streaming applications executed on multiprocessor systems with processor sharing and SPP scheduling that can be expressed using Cyclo-Static Dataflow (CSDF) models. This allows to model tasks with multiple phases and changing rates and furthermore resolves the problematic restriction that buffer synchronization must occur atomically at the boundaries of task executions. For that purpose a joint interference characterization over multiple phases is introduced, which realizes a significant accuracy improvement compared to an isolated consideration of interference. Applicability, efficiency and accuracy of the presented approach are evaluated in a case study using a WLAN 802.11p transceiver application. Thereby different use-cases of CSDF modeling are discussed, including a CSDF model relaxing the requirement of atomic synchronization.
Web content changes rapidly [18]. In Focused Web Harvesting [17] which aim it is to achieve a complete harvest for a given topic, this dynamic nature of the web creates problems for users who need to access a set of all the relevant web data to their topics of interest. Whether you are a fan following your favorite idol or a journalist investigating a topic, you may need not only to access all the relevant information but also the recent changes and updates. General search engines like Google apply several techniques to enhance the freshness of their crawled data. However, in focused web harvesting, we lack an efficient approach that detects changes for a given topic over time. In this paper, we focus on techniques that can keep the relevant content to a given query up-to-date. To do so, we test four different approaches to efficiently harvest all the changed documents matching a given entity by querying web search engines. We define a document with changed content or a newly created or removed document as a changed document. Among the proposed change detection approaches, the FedWeb method outperforms the other approaches in finding the changed content on the web for a given query with 20 percent, on average, better performance.
Programmable Logic Controllers (PLCs) are a family of embedded devices used for physical process control. Similar to other embedded devices, PLCs are vulnerable to cyber attacks. Because they are used to control the physical processes of critical infrastructures, compromised PLCs constitute a significant security and safety risk. In this paper, we investigate attacks against PLCs by introducing a specific type of attack against a PLC that allows the adversary to stealthily manipulate the physical process it controls by tampering with the device I/O at a low level. We implemented two variant of the attack in the form of a rootkit and a user-space malicious code over a candidate PLC. However in this technical edition we do not include the design information of the rootkit or the user-space malicious software. Our study is meant to be used as a basis for the design of more robust detection techniques specifically tailored for PLCs.
Batteries are omnipresent, and with the uprise of the electrical vehicles will their use will grow even more. However, the batteries can deliver their required power for a limited time span. They slowly degrade with every charge-discharge cycle. This degradation needs to be taken into account when considering the battery in long lasting applications. Some detailed battery models that describe the degradation exist. However, these are complex models that require detailed knowledge. These models are in general computationally intensive, which does not make them well suited to be used in a wider context. A model better suited for this is the Kinetic Battery Model. In this paper, we this model would change due to battery degradation, by the results of our experimental degradation analysis. In our analysis we see that the degradation takes place in two phases. After the first phase of slow degradation, the battery suddenly starts to degrade rapidly.
Risk assessment of unavailability of telecommunication services is an important part of an organisation’s business continuity management. We developed the Raster method to enable organisations to assess their telecommunication service unavailability risks. To validate Raster in practice we conducted two field tests in which the Raster method was applied at a typical target organisation. This document reports on the second field test, at a Water Board in the Netherlands. This report describes the research goals, method, and results of this field test, and compares the results to those of the first field test. This field test reconfirms the usefulness of the Raster method, and adds some new lessons-learned.
System lifetime is a major design constraint for battery-powered mobile embedded systems. The increasing gap between the energy demand of portable devices and their battery capacities is further limiting durability of mobile devices. Thus, the guarantees over Quality of Service (QoS) of batteryconstrained devices under strict battery capacities are of primary interest for mobile embedded systems' manufacturers and stakeholders.This paper presents a novel approach for deriving QoS of applications modelled as synchronous dataflow (SDF) graphs. We map these applications on heterogeneous multiprocessor platforms that are partitioned into Voltage and Frequency Islands, together with multiple kinetic battery models (KiBaMs). By modelling the whole system as hybrid automata, and applying model-checking, we evaluate, (1) system lifetime; and (2) minimum required initial battery capacities to achieve the desired application performance. We demonstrate that our approach shows a significant improvement in terms of scalability, as compared to a priced timed automata based KiBaM model. This approach also allows early detection of design errors via model checking.
Hardware-software (HW-SW) co-design allows to meet system-level objectives by exploiting the synergy of hardware and software. Current tools and approaches for HW-SW co-design face difficulties coping with the increasing complexity of modern-day application due to, e.g., concurrency and energy constraints. Therefore, an automated modeling approach is needed which satisfies modularity, extensibility and interoperability requirements. Model-Driven Engineering (MDE) is a prominent paradigm that, by treating models as first-class citizens, helps to fulfill these requirements. This paper presents a state-of-the-art MDE-based framework for HW-SW co-design of dataflow applications, based on synchronous dataflow (SDF) graph formalism. In the framework, we introduce a reusable set of three coherent metamodels for creating HW-SW co-design models concerning SDF graphs, hardware platforms and allocation of SDF tasks to hardware. The framework also contains model transformations that cast these models into priced timed-automata models, the input language of the well-known model checker uppaal cora. We demonstrate how our framework satisfies the requirements of modularity, extensibility and interoperability in an industrial case study.
Socio-technical models are models that represent social as well as technical elements of the modeling subject, where the technical part consists of both physical and digital elements. Examples are enterprise models and models of the target of assessment used in risk assessment. Constructing and validating these models often implies a challenging task of extracting and integrating information from a multitude of stakeholders which are rarely modelling experts and don’t usually have the time or desire to engage in modelling activities. We investigate a promising approach to overcome this challenge by using physical tokens to represent the model. We call the resulting models tangible models. In this paper we illustrate this idea by creating a tangible representations of a socio-technical modelling language used in Risk Assessment and provide an initial validation of the relative usability and utility of tangible versus abstract modelling by an experiment and a focus group, respectively. We discuss possible psychological and social mechanisms that could explain the enhanced usability and utility of tangible modelling approaches for domain experts. Finally, we discuss the generalizability of this approach to other languages and modelling purposes.
Execution time is no longer the only performance metric for computer systems. In fact, a trend is emerging to trade raw performance for energy savings. Techniques like Dynamic Power Management (DPM, switching to low power state) and Dynamic Voltage and Frequency Scaling (DVFS, throttling processor frequency) help modern systems to reduce their power consumption while adhering to performance requirements. To balance flexibility and design complexity, the concept of Voltage and Frequency Islands (VFIs) was recently introduced for power optimisation. It achieves fine-grained system-level power management, by operating all processors in the same VFI at a common frequency/voltage.This paper presents a novel approach to compute a power management strategy combining DPM and DVFS. In our approach, applications (modelled in full synchronous dataflow, SDF) are mapped on heterogeneous multiprocessor platforms (partitioned in voltage and frequency islands). We compute an energy-optimal schedule, meeting minimal throughput requirements. We demonstrate that the combination of DPM and DVFS provides an energy reduction beyond considering DVFS or DMP separately. Moreover, we show that by clustering processors in VFIs, DPM can be combined with any granularity of DVFS. Our approach uses model checking, by encoding the optimisation problem as a query over priced timed automata. The model-checker Uppaal Cora extracts a cost minimal trace, representing a power minimal schedule. We illustrate our approach with several case studies on commercially available hardware.
In the “The curse of simultaneity”, Paes Leme et al. show that there are interesting classes of games for which sequential decision making and corresponding subgame perfect equilibria avoid worst case Nash equilibria, resulting in substantial improvements for the price of anarchy. This is called the sequential price of anarchy. A handful of papers have lately analysed it for various problems, yet one of the most interesting open problems was to pin down its value for linear atomic routing (also: network congestion) games, where the price of anarchy equals 5/2. The main contribution of this paper is the surprising result that the sequential price of anarchy is unbounded even for linear symmetric routing games, thereby showing that sequentiality can be arbitrarily worse than simultaneity for this class of games. Complementing this result we solve an open problem in the area by establishing that the (regular) price of anarchy for linear symmetric routing games equals 5/2. Additionally, we prove that in these games, even with two players, computing the outcome of a subgame perfect equilibrium is 𝖭𝖯 -hard.
One of the main challenges in developing a software system is to assure that its properties fulfill the specifications. In the context of this paper, we are especially interested in timing properties. Model-based software verification is one of the approaches to achieve this. However, model-based verification requires expressive models of software systems and deriving such models is not a trivial task. Although there are a few model derivation tool proposals for the purpose of model-checking timing properties, these are dedicated tools supporting a selected set of verification techniques and as such they are not explicitly designed for coping with new demands. This paper presents a framework that derives models from Java programs in an automated way for analyzing timing properties. The framework has the following properties that are not provided by the previous proposals: (1) Efficiency in model development, (2) consistency of models with software, (3) expressiveness of models, (4) scalability and (5) extensibility of the model derivation process.
We propose a new score function to compare and evaluate the relative impact of state-of-charge profiles on overall battery lifetime. Our score function, based on on a discrete Fourier transform of the state-of-charge profile, formalizes and generalizes earlier ideas found in the literature, and can form an important help in optimizing overall life time for battery powered systems. In this paper we introduce and illustrate the method, and discuss its merits as well as open issues and related literature.
As part of the EU FP7 project SPENCER a robot demonstrator will be developed which provides location based services (information, guiding) to passengers in the context of an international airport. In this report we describe a contextual analysis, conducted in order to discover how people behave in a given context (here Schiphol airport) and in relevant situations within this context. From this analysis we arrive at guidelines for robot behavior.
Telecommunication services are complex product packages that rely on a large and complex technical infrastructure. However, fraudulent use of such telecommunication services rarely exploits hardware vulnerabilities. Instead, most common exploits operate at a business level, capitalizing on the unexpected interaction between various product packages from multiple providers. As such, an assumption was made that in order to fully describe the scenarios, a modelling language capable of describing value transactions between actors is required. In order to validate this assumption, a business value modelling language, e3value was selected, generic (non-misuse) business models were created and four misuse scenarios were modelled. This report showcases the models, discusses strengths and limitations encountered during modelling and draws conclusions with regard to the applicability, usability and utility of e3value models in modelling (Telecom) fraud as well as more generally in Risk Assessment.
Costs and rewards are important ingredients for many types of systems, modelling critical aspects like energy consumption, task completion, repair costs, and memory usage. This paper introduces Markov reward automata, an extension of Markov automata that allows the modelling of systems incorporating rewards (or costs) in addition to nondeterminism, discrete probabilistic choice and continuous stochastic timing. Rewards come in two flavours: action rewards, acquired instantaneously when taking a transition; and state rewards, acquired while residing in a state. We present algorithms to optimise three reward functions: the expected cumulative reward until a goal is reached, the expected cumulative reward until a certain time bound, and the long-run average reward. We have implemented these algorithms in the SCOOP/IMCA tool chain and show their feasibility via several case studies.
