This paper presents a unified formal framework, called ReTA, that allows users to definescheduling problemsusing a user-friendly domain-specific language (DSL) and automatically obtain response times of jobs in return. ReTA supports user-defined online scheduling policies (beyond work-conserving or priority-based scheduling) for heterogeneous computing resource types with multiple instances per type (e.g., multiple CPU cores, GPUs, DSPs, and FPGAs on one single chip), thus supporting global, partitioned, and clustered scheduling. In the current version of ReTA, we focus on non-preemptive periodic tasks as these are susceptible to scheduling anomalies and hence harder to analyze. ReTA performs response-time analysis by constructing atimed labeled transition system(TLTS) from the domain model as a basis for performing a reachability analysis enriched with efficient state-space reduction techniques. Our empirical evaluations show that ReTA identifies up to50 times more schedulable task setsthan fixed-point iteration-based analyses. With a runtime on the order of a few minutes, ReTA produces highly accurate resultstwo-orders of magnitude fasterthan an exact Timed Automata-based analysis in UPPAAL (e.g., for systems with 16 cores and 32 tasks).

Real-time systems are commonly used in safety-critical applications which require tasks to be completed before their deadlines, even in the presence of faults. Thus, fault tolerance becomes essential to ensure a certain level of reliability in safety-critical real-time systems [1]. To achieve fault tolerance in computer systems, redundancy can be implemented either in space (spatial redundancy) or time (time redundancy) [2]. Unlike spatial redundancy which involves increasing hardware resources, time redundancy focuses on re-execution or multiple executions of software on the same hardware resources [3] and therefore is better suited for embedded systems with limited cost and size constraints that are subject to transient faults more often than permanent faults [2], [4].

While multicore real-time systems are extensively employed in the industry, research gaps still exist in developing a scalable analysis to find tight bounds on the worst-case response time (WCRT) of tasks scheduled by global preemptive scheduling policies. Additionally, the presence of release jitter poses a challenge where examining the earliest and latest release times may not derive WCRT. The existing analyses either provide very conservative bounds or face challenges in scaling to systems with numerous cores and tasks. This work provides preliminary foundations to derive tight WCRT bounds for tasks scheduled by global preemptive job-level fixed-priority scheduling policies (e.g., EDF and FP) on homogeneous multicore platforms by performing a reachability analysis using time-label-transition systems. Our solution uses 2 orders of magnitude less memory than UPPAAL and identifies on average 12% (up to 39%) more schedulable task sets than sufficient schedulability analyses (e.g., for systems with 4 cores and 10 tasks).

System-Performance Engineering (SysPE) encompasses modeling formalisms, methods, techniques, and industrial practices to design systems for performance, where performance is taken integrally into account during the whole system life cycle. Industrial SysPE state of practice is generally model-based. Due to the rapidly increasing complexity of systems, there is a need to develop and establish model-driven methods and techniques. To structure the field of SysPE, we identify (1) industrial challenges motivating the importance of SysPE, (2) scientific challenges that need to be addressed to establish model-driven SysPE, (3) important focus areas for SysPE and (4) best practices. We conducted a survey to collect feedback on our views. The responses were used to update and validate the identified challenges, focus areas, and best practices. The final result is presented in this paper. Interesting observations are that industry sees a need for better design-space exploration support, more than for additional performance modeling and analysis techniques. Also tools and integral methods for SysPE need attention. From the identified focus areas, scheduling and supervisory control is seen as lacking established best practices.

This article presents a modular automaton-based framework to specify flexible manufacturing systems and to optimize the makespan of product batches. The Batch Makespan Optimization (BMO) problem is NP-Hard and optimization can therefore take prohibitively long, depending on the size of the state-space induced by the specification. To tame the state-space explosion problem, we develop an algebra based on automata equivalence and inclusion relations that consider both behavior and structure. The algebra allows us to systematically relate the languages induced by the automata, their state-space sizes, and their solutions to the BMO problem. Further, we introduce a novel constraint-based approach to systematically prune the state-space based on the the notions of nonpermutation-repulsiveness and permutation-attractiveness. We prove that constraining a nonpermutation-repulsing automaton with a permutation-attracting constraint always reduces the state-space. This approach allows us to (i) compute optimal solutions of the BMO problem when the (additional) constraints are taken into account and (ii) compute bounds for the (original) BMO problem (without using the constraints). We demonstrate the effectiveness of our approach by optimizing an industrial wafer handling controller.

We develop a model-based approach to predict timing of service-based software applications on Linux-based multi-core platforms for alternative mappings (affinity and priority settings). Service-based applications consist of communicating sequential (Linux) processes. These processes execute functions (also called services), but can only execute them one at a time. Models are inferred automatically from execution traces to enable timing optimization of existing (legacy) systems. Our approach relies on a linear progress approximation of functions. We compute the expected share of each function based on the mapping (affinity and priority) parameters and the functions that are currently active. We validate our models by carrying out a controlled lab experiment consisting of a multi-process pipelined application mapped in different ways on a quadcore Intel i7 processor. A broad class of affinity and priority settings is fundamentally unpredictable due to Linux binding policies. We show that predictability can be achieved if the platform is partitioned in disjoint clusters of cores such that i) each process is bound to such a cluster, ii) processes with non real-time priorities are bound to singleton clusters, and iii) all processes bound to a non-singleton cluster have different real-time priorities. For mappings using singleton clusters with niceness priorities only, our model predicts execution latencies (for each pipeline iteration) with errors less than 5% relative to the measured execution times. For mappings using a non-singleton cluster (with different real-time priorities) relative errors of less than 2% are obtained. When real-time and niceness priorities are mixed, we predict with errors of 7%.

In this paper we address the makespan optimization of industrial-sized manufacturing systems. We introduce a framework which specifies functional system requirements in a compositional way and automatically computes makespan optimal solutions respecting these requirements. We show the optimization problem to be NP-Hard. To scale towards systems of industrial complexity, we propose a novel approach based on a subclass of compositional requirements which we call constraints. We prove that these constraints always prune the worst-case optimization-space thereby increasing the odds of finding an optimal solution (with respect to the additional constraints). We demonstrate the applicability of the framework on an industrial-sized manufacturing system.

System design is a difficult process with many design-choices for which the impact may be difficult to foresee. Manufacturing system design is no exception to this. Increased use of flexible manufacturing systems which are able to perform different operations/use-cases further raises the design complexity. One important criterion to consider is the overall makespan and associated critical path for the different use-cases of the system. Stochastic critical path analysis plays a fundamental role in providing useful feedback for system designers to evaluate alternative specifications, which traditional fixed-time analysis cannot. In this paper, we extend our formal model-based framework, for the specification and design of manufacturing systems, with stochastic analysis abilities by associating a criticality index to each action performed by the system. This index can then be visualized and used within the framework such that a system designer can make better informed decisions. We propose a Monte-Carlo method as an estimation algorithm and we explicitly define and use confidence intervals to achieve an acceptable estimation error. We further demonstrate the use of the extended framework and stochastic analysis with an example manufacturing system.

This paper introduces a formal modeling approach for compositional specification of both functionality and timing of manufacturing systems. Functionality aspects can be considered orthogonally to timing aspects. The functional aspects are specified using two abstraction levels; high-level activities and lower level actions. Design of a functionally correct controller is possible by looking only at the activity level, abstracting from the different execution orders of actions and their timing. As a result, controller design can be performed on a much smaller state space compared to an explicit model where timing and actions are present. The performance of the controller can be analyzed and optimized by taking into account the timing characteristics. Since formal semantics are given in terms of a (max, +) state space, various existing performance analysis techniques can be used. We illustrate the approach, including performance analysis, on an example manufacturing system.

This paper proposes a modeling approach to capture the mapping of an application on a platform. The approach is based on Scenario-Aware Dataflow (SADF) models. In contrast to the related work, we express the complete design-space in a single formal SADF model. This allows us to have a compact and explorable state-space linked with an executable model capable of symbolically analyzing different mappings for their timing behavior. We can model different bindings for application tasks, different static-orders schedules for tasks bound in shared resources, as well as naturally capturing resource claiming/unclaiming using SADF semantics. Moreover, by using the inherent properties of dataflow graphs and the dynamic behavior of a Finite-State Machine, we can model different levels of pipelining, such as full application pipelining and interleaved pipelining of consecutive executions of the application. The size of the model is independent of the number of executions of the application. Since we are able to capture all this behavior in a single SADF model we can use available dataflow analysis, such as worst-case and best-case throughput and deadlock-freedom checking. Furthermore, since the model captures the design-space independently of the analysis technique, one can use different exploration approaches to analyze different sets of requirements.

Development of high-level supervisory controllers is an important challenge in the design of high-tech systems. It has become a significant issue due to increased complexity, combined with demands for verified quality, time to market, ease of development, and integration of new functionality. To deal with these challenges, model-based engineering approaches are suggested as a cost-effective way to support easy adaptation, validation, synthesis, and verification of controllers. This paper presents an industrial case study on modular design of a supervisory controller for wafer logistics in lithography machines. The uncontrolled system and control requirements are modeled independently in a modular way, using small, loosely coupled and minimally restrictive extended finite automata. The multiparty synchronization mechanism that is part of the specification formalism provides clear advantages in terms of modularity, traceability, and adaptability of the model. We show that being able to refer to variables and states of automata in guard expressions and state-based requirements, enabled by the use of extended finite automata, provides concise models. Additionally, we show how modular synthesis allows construction of local supervisors that ensure safety of parts of the system, since monolithic synthesis is not feasible for our industrial case.

Analyzing worst-case application timing for systems with shared resources is difficult, especially when non-monotonic arbitration policies like First-Come-First-Served (FCFS) scheduling are used in combination with varying task execution times. Analysis methods that conservatively analyze these systems are often based on state-space exploration, which is not scalable due to its inherent susceptibility to combinatorial explosion. We propose a scalable timing analysis method on periodically restarted Directed Acyclic Task Graphs, that can provide conservative bounds on task timing properties when shared resources with FCFS scheduling are used. By expressing task enabling and completion times in intervals, denoting best-case and worst-case timing properties, contention on the shared resources can be estimated using conservative approximations. With an industrial case study we show that our approach can easily analyze models with thousands of tasks in less than 10 seconds, and the worst-case bounds obtained show an average improvement of 46% compared to bounds obtained by static worst-case analysis.

Latest trends in embedded platform architectures show a steady shift from high frequency single core platforms to lower-frequency but highly-parallel execution platforms. Scheduling applications with stringent latency requirements on such multiprocessor platforms is challenging. Our work is motivated by the scheduling challenges faced by ASML, the world's leading provider of wafer scanners. A wafer scanner is a complex cyber-physical system that manipulates silicon wafers with extreme accuracy at high throughput. Typical control applications of the wafer scanner consist of thousands of precedence-constrained tasks with latency requirements. Machines are customized so that precise characteristics of the control applications to be scheduled and the execution platform are only known during machine start-up. This results in large-scale scheduling problems that need to be solved during start-up of the machine under a strict timing constraint on the schedule delivery time. This paper introduces a fast and scalable static-order scheduling approach for applications with stringent latency requirements and a fixed binding on multiprocessor platforms. It uses a heuristic that makes scheduling decisions based on a new metric to find feasible schedules that meet timing requirements as quickly as possible and it is shown to be scalable to very large task graphs. The computation of this metric exploits the binding information of the application. The approach will be incorporated into the ASML's latest generation of wafer scanners.

To provide a good balance between the performance and flexibility of future digital control platforms, we propose an FPGA-based heterogeneous multiprocessor approach, in which the platform is composed of processing elements from a set of parameterizable heterogeneous Application-Specific Instruction-set Processors (ASIPs), connected with an hierarchical interconnect. With a case-study treating two different industrial-scale controllers, we show that a platform generated from our template using only a small library of instantiable ASIP types outperforms an optimized 8-core general-purpose implementation by a factor 4.9 on sampling frequency and reduces IO-delay with 37.5%.

Performance modeling of embedded systems is used to explore the system-level design-space and compare a wide range of possible solutions with respect to their performance gain. Calibration and validation of the developed performance models help ensure that the performance predictions of these models are accurate. This paper presents formal definitions of the errors associated with the calibration and prediction process. In addition to a quantitative description of these errors, this paper also provides formal means to estimate their upper bounds, based on known or measured quantities.

The complexity of designing hardware/software systems motivates research on frameworks that structure and automate the design process. Such design methodologies reduce the risk of expensive design-implementation iterations by assisting designers in constructing models. Software/hardware engineering (SHE) is a general-purpose system-level design methodology that supports analysing both functional correctness and performance properties. SHE combines the Unified Modelling Language with the parallel object-oriented specification language to specify models. The designer is assisted in constructing models using these languages and applying the analysis techniques with various guidelines and modelling patterns. A key feature of SHE is its foundation on formal methods, which ensures that the obtained analysis results are unambiguous. SHE also includes guidelines and techniques for automatic synthesis of real-time control software. This is again based on formal methods to ensure that properties in a model (including real-time properties) are preserved by the software realisation. Finally, to enable an effective and efficient application of the modelling languages as well as the analysis and synthesis techniques, SHE is accompanied with a set of user-friendly tools. This paper gives an overview of SHE, thereby briefly touching upon the underlying mathematical foundation of the analysis and synthesis techniques as well as upon some open issues that require further research.

Formal theories for real-time systems (such as timed process algebra, timed automata and timed petri nets) have gained great success in the modeling of concurrent timing behavior and in the analysis of real-time properties. However, due to the ineliminable timing differences between a model and its realization, synthesizing a software realization from a model in a predictable way is still a challenging research topic. In this article, we tackle this problem by solving a set of sub-problems. The solution is based on the theoretical results for property prediction proposed in Huang et al. ( 2003 , Real-time property preservation in approximations of timed systems. In: Proceedings of 1st ACM and IEEE international conference on formal methods and models for codesign. IEEE Computer Society, Los Alamitos, pp 163–171) and Huang ( 2005 , Predictability in real-time system design. PhD thesis, Eindhoven University of Technology, The Netherlands), where quantitative property relations are established between two absolute/relative “close” real-time systems. This theory basically implies that if two systems are “close”, they enjoy “similar” properties. These results cannot be directly applied in practice though, because a model and its realization typically have infinitely large absolute and relative timing differences. We show that this infinite time gap can be bridged through a sequence of carefully constructed intermediate time domains. Then the property-prediction results can be applied to any pair of adjacent time domains in the sequence. Consequently, real-time properties of the implementation can be predicted from the model. We propose two parameterized hypotheses to characterize the timing differences in the sequence and to guide a correctness-preserving design process. It is shown that these hypotheses can be incorporated in a concrete tool set. We demonstrate the feasibility of the predictable synthesis approach through the design of a railroad crossing system.

Data flow models are used for specifying and analysing signal processing and streaming applications. However, traditional data flow models are either not capable of expressing the dynamic aspects of modern streaming applications or they do not support relevant analysis techniques. The dynamism in modern streaming applications often originates from different modes of operation (scenarios) in which data production and consumption rates and/or execution times may differ. This paper introduces a scenario-aware generalisation of the synchronous data flow model, which uses a stochastic approach to model the order in which scenarios occur. The formally defined operational semantics of a scenario-aware data flow model implies a Markov chain, which can be analysed for both long-run average and worst-case performance metrics using existing exhaustive or simulation-based techniques. The potential of using scenario-aware data flow models for performance analysis of modern streaming applications is illustrated with an MPEG-4 decoder example

To build a "correct" implementation from a model of a concurrent real-time system, it is important to understand the relation between the properties of the model and of its corresponding implementation. In this paper, the behaviour of a system is described with timed action sequences. Based on a notion of distance that expresses the observable property preservation between timed action sequences, we show that a stronger observable property preservation between model and implementation is obtained when urgency on the execution of observable actions is imposed over the execution of unobservable ones. Furthermore, we present a model synthesis approach and, by means of a case study, we show how it can be applied in the synthesis of real-time systems.

Formal techniques have been widely applied in the design of real-time systems and have significantly helped detect design errors by checking real-time properties of the model. However, a model is only an approximation of its realization in terms of the issuing time of events. Therefore, a real-time property verified in the model can not always be directly transferred to the realization. In this paper, both the model and the realization are viewed as sets of timed state sequences. In this context, we first investigate the real-time property preservation between two neighboring timed state sequences (execution traces of timed systems), and then extend the results to two "neighboring" timed systems. The study of real-time property preservation gives insight in building a formal link between real-time properties satisfied in the model and those in the realization.

We discuss the gap we experience in an industrial design path of high-speed packet switches. As bandwidth demand exceeds progress in CMOS technology, system architects are forced to abandon familiar design solutions and make fundamental changes to their architectures at an increasingly faster pace. We investigate design methods to decrease the risk of such changes and to provide a structured and confident transition from conceptual system-level models to hardware descriptions. It appears that the design gap is caused by differences between language primitives and underlying concepts of system-level design languages and hardware description languages. We substantiate the need for expressive system-level modeling concepts and show that the gap is actually caused by a fundamental interpretation mismatch between models and descriptions. Based on a comparison of existing system-level synthesis methods with the interpretation gap, we propose to decrease the gap by using modeling patterns.

The completeness of a collection of design transformations is an important aspect in transformational design. Completeness guarantees that any correct design can in principle be explored using the transformation system. In the field of transformational design the problem of incompleteness is not well understood and it is often believed that complete transformation systems can be constructed. In this article, we show, using a formal framework based on the theory of computation, that this is not the case if the transformation system is based on an expressive general-purpose design language such as VHDL. Only when restrictions are imposed on the design language and correctness relation, a transformation system can be made complete in theory, but this is expected to result in serious practical problems. It is shown that the incompleteness problem in transformational design is closely related to the syntactic variance problem in high-level synthesis and that this latter problem is not solvable in general either.