Search

Dataflow formalisms are useful for specifying signal processing and streaming applications. To adequately capture the dynamic aspects of modern applications, the formalism of Scenario-Aware Dataflow (SADF) was recently introduced, which allows analysis of worst/best-case and average-case performance across different modes of operation (scenarios). The semantic model of SADF integrates non-deterministic and discrete probabilistic behaviour with generic discrete time distributions. This combination is different from the semantic models underlying contemporary quantitative model checking approaches, which often assume exponentially distributed or continuous time or they lack support for expressing discrete probabilistic behaviour. This paper discusses a model-checking approach for computing quantitative properties of SADF models such as throughput, time-weighted average buffer occupancy and maximum response time. A compositional state-space reduction technique is introduced as well as an efficient implementation of this method that combines model construction with on-the-fly state-space reductions. Strong reductions are possible because of special semantic properties of SADF, which are common to dataflow models. We illustrate this efficiency with several case studies from the multi-media domain.

Embedded control is a key product technology differentiator for many high-tech industries, including ASML. The strong increase in complexity of embedded control systems, combined with the occurrence of late changes in control requirements, results in many timing performance problems showing up only during the integration phase. The fallout of this is extremely costly design iterations, severely threatening the time-to-market and time-to-quality constraints. This paper reports on the industrial application at ASML of the Y-chart method to attack this problem. Through the largely automated construction of executable models of a wafer scanner's mechatronics control application and platform, ASML was able to obtain high-level overview early on in the development process. The system wide insight in timing bottlenecks gained this way resulted in more than a dozen improvement proposals yielding significant performance gains. These insights also led to a new development roadmap of the mechatronics control execution platform.

POOSL (Parallel Object-Oriented Specification Language) is a powerful general purpose system-level modeling language. In research on design space exploration of motion control systems, POOSL has been used to construct models for performance analysis. The considered motion control algorithms are characterized by periodic execution. They are executed by multiple processors, which are interconnected by Rapid Input/Output (RapidIO) packet switches. Packet latencies as worst-case latencies and average-case latencies are essential performance criteria for motion control systems. However, POOSL analysis merely allows for estimation results for these latency metrics since it is primarily based on simulation. Because motion control systems are time-critical and safety-critical, worst-case latencies of packets are strict timing constraints. Therefore exact worst-case latencies are to be determined. Motivated by this requirement we propose to use model checking techniques. In this paper we illustrate how a POOSL model of a (simplified) motion control system can be transformed into an UPPAAL model and we verify its functional behavior and worst-case latencies. Moreover, we show that analysis of average-case latencies can also be accomplished with assistance of the model checking tool UPPAAL.

Embedded systems are a source of technology that facilitates our modern lifestyle. In order to do so, they tend to increase in complexity as well as integrate in are day-to-day activities. To meet the market's expectations on technological improvement, time-to-market objectives for introducing innovative embedded systems are shorter than ever. Over the last decade, model-based design has been a subject of great interest as a means to accelerate the design of embedded systems. The Y-chart paradigm is a principal approach to model-based embedded system design. Despite the simplicity and conciseness of this paradigm, it has been implemented in several di®erent ways by various methodologies. This variety in implementation designs is due to the particular emphasis a methodology puts on the di®erent steps of the paradigm (application modeling, platform modeling, mapping, analysis and synthesis). This article explores this variety by examining and comparing three Y-chart based design methodologies: Metropolis, the Distributed Operation Layer incorporating Modular Performance Analysis and the Y-chart variant of the Software/Hardware Engineering methodology. These methodologies have been chosen because they: cover a broad domain of applications, have been developed on a relatively long period of time and are representative of typical Y chart approaches. Moreover, these implementations of the paradigm present interesting design approaches which are worth comparing

Multi-processor system-on-chip (MPSoC) design is profiting considerably from the trend towards model-driven design. Design choices in this area cover considerations on alternative parallellisations of application software, alternative architectures for the hardware platform and different ways to map applications onto the platform. Various paradigms exist for modelling applications and also for modelling platforms. This paper presents a tool for generating abstract performance models of MPSoC systems to further automate their design-space exploration. The tool supports several traditional paradigms for specifying applications and uses a new model of architecture to enable describing hardware platforms at a much higher abstraction level than traditional hardware description languages. The tool relies on a collection of modelling patterns to convert application and platform specifications together with a mapping into one unifying model expressed in a formal general-purpose modelling language that offers extensive support for performance analysis.

The Parallel Object-Oriented Specification Language (POOSL) is an expressive modelling language for hardware/software systems [10]. It was originally defined in [7] as an object-oriented extension of process algebra CCS [6], supporting (conditional) synchronous message passing between (hierarchically structured) asynchronous concurrent processes. Meanwhile, POOSL has been extended with real-time [2] and probabilities [I] to evolve into a powerful general-purpose modelling language accompanied with simulation, analysis and synthesis techniques that scale to large industrial design problems.

The design of complex real-time distributed hardware/software systems commonly involves evaluating the performance of several design alternatives. Early in the design process, it is therefore desirable that design methods support constructing abstract models for the purpose of analysis. Recent extensions to the Unified Modeling Language (UML) that enable specifying schedulability, performance and time provide a means to start developing such models directly after defining the concepts and requirements of a system. However, UML hampers the evaluation of performance properties because this requires constructing executable models with a modeling language that supports application of mathematical analysis techniques. In this paper, we present how the Software/Hardware Engineering (SHE) method can be used for the performance modeling of real-time distributed hardware/software systems. Starting from a UML specification, SHE enables constructing formal executable models based on the expressive modeling language POOSL (Parallel Object-Oriented Specification Language).

To satisfy the severe requirements involved in future communication networks, commercial and research interest in the applicability of wavelength division multiplexing (WDM) is growing. However, since WDM is merely concerned with transmitting bits over optical fibers, full advantage can only be taken when WDM is efficiently supported by higher-layer protocols. Functionality of higher-layer protocols that could be used in conjunction with WDM originates from synchronous digital hierarchy (SDH) or synchronous optical network (SONET), asynchronous transfer mode (ATM), and the internet protocol (IP). To provide flexible use of services with different levels of quality, various higher-layer protocols may directly support WDM simultaneously by reserving wavelength channels for a specific supporting protocol. Focussing on aspects of network management, this paper investigates how the mentioned higher-layer protocols may concurrently support WDM.

A major problem in performance evaluation of real-life industrial systems is the enormous number of states generated by the system's model during the simulation process. An example is in a Parallel Object-Oriented Specification Language (POOSL) model, which can be interpreted as a discrete-time Markov chain enabling the evaluation of long-run average performance metrics. In general this Markov chains is huge, making performance simulation expensive since all performance estimations must be updated in each state. In this paper, we introduce a method for performance evaluation based on Markov chain theory, which aims at the reduction of the original Markov chain into a smaller chain. We prove that the reduction yields another Markov chain and it preserves several important properties. We further give a method to effectively construct the reduced chain. The reduction method yields an efficient way to estimate performance metrics during model simulation, since in general it requires estimations to be updated only in a relatively small part of the state space.

Before implementing a system with hardware and software components, performance modelling is often used for evaluating design alternatives. The formal modelling language Parallel Object-Oriented Specification Language (POOSL) has proven to be very useful for analysing performance metrics of design alternatives for real-life industrial systems. Based on its mathematically defined semantics, POOSL enables to analytically compute performance metrics by analysing the Markov chain that is implicitly defined by a POOSL model. Models of real-life industrial systems are however often too complex to be analysed exhaustively. Performance evaluation is therefore based on simulation, enabling the estimation of performance metrics. However, simulation results only have a proper meaning if their accuracy is known. In general, longer simulation yields more accurate results. To analyse the accuracy of simulation results and automatically terminate the simulation after accurate results have been obtained, confidence intervals can be used. Based on the properties of the Markov chains implicitly defined by POOSL models, this paper presents a technique of regenerative cycles for analysing the accuracy of long-run sample average estimation. Furthermore, an algebra of confidence intervals is defined to enable accuracy analysis of long-run time averages as well as long-run sample and time variances. Finally, library classes are introduced for POOSL, which ease accuracy analysis for the mentioned performance metric types.