Model-Implementation Fidelity in Cyber Physical System Design

In this chapter, we overview some of the sought challenges for building faithful embedded systems models. We highlight the growing demand for using formal models especially for dealing with performance. The chapter illustrates the impact of the hardware part of the system on performance and suggests a probabilistic interpretation in order to build appropriately abstract models towards trustworthy analysis. We believe that such a view is worth to investigate to faithfully characterize the system performance as it provides a formal and parsimonious framework. In this context, we survey some probabilistic models and techniques that we think interesting for building such faithful representations.

Model complexity is a major concern affecting the design, analysis and runtime management of computing systems. One way of dealing with model complexity is to compromise on the fidelity of a model’s representation of entities and issues that the model is supposed to represent. This chapter describes a resource-driven modelling approach whereby the fidelity of a model can be managed rationally in order to control model complexity. This approach includes two concrete and related methods targeting two aspects of the problem. Dynamic resource graphs highlight the dependencies between system resources and describe a system’s progression as resource and dependency evolution steps. This forms a theoretical foundation for the tracking of parameters that can be regarded as resources, e.g. power consumption, time, computation units, etc. With this resource-oriented view of a system, a hierarchical modelling method emphasizing cross-layer cuts is established. This method facilitates parameter-proportional modelling to achieve optimal fidelity vs complexity trade-offs in models. Simulation and state space analysis application use cases help to validate the approach.

With the predicted device, core, and multi-core scaling, a recent study revealed that regardless of chip organization and topology, multi-core scaling is power limited. It has been predicted that at 22 nm, 21 % of a fixed-size chip must be powered off, and at 8 nm, even more than 50 % (Esmaeilzadeh et al., News 39(3):365–376, 2011). Especially for mixed-criticality systems, which consist of a mixture of safety and non-safety relevant applications, this is of major concern. Safety-critical applications cannot be simply switched on and off or migrated during run-time. A system engineer should be aware of any possible cross-application interferences with respect to timing, power, and thermal properties as soon as possible in the design process. Introduction of power and temperature management must be planned and realized without violating freedom from interference. For this reason, the extra-functional properties need to be modeled and analyzed at the system level, because they can strongly affect the overall quality of service (performance, battery lifetime) or even cause the system to fail meeting its real-time and safety requirements.In this chapter, we present our vision of a SystemC-based simulation framework for capturing extra-functional properties in virtual platforms, currently under development in the CONTREX project. This covers the specification of platform properties (extra-functional model) as well as the dynamic capturing, processing, and extraction of power/temperature information during the simulation. Especially closing the loop back to the application and run-time services is an important feature for complex heterogeneous hardware platforms and software stacks. As an example, we will present a battery-powered mixed-critical avionics system, running a safety-critical flight control application and a performance critical image processing application on the same multi-core System on Chip.

Synchronous dataflow (SDF) graphs are often the computational model of choice for specification, analysis, and automated synthesis of parallel streaming kernels targeting embedded multiprocessor system-on-a-chip (MPSoC) platforms. We discuss several limitations of the SDF graphs in the context of conventional parallel software synthesis methodologies, and highlight the associated degradation in analysis accuracy and performance of the synthesized software. Subsequently, we propose several extensions to the strict notion of SDF graph model that address the identified issues. We present extensive empirical evaluations, which underscore the model limitations and the effectiveness of our approach.

This chapter presents the SimSoC virtual prototyping framework, a full system simulation framework, based on SystemC and Transaction Level Modeling. SimSoC takes as input a binary executable file, which can be a full operating system, and simulates the behavior of the target hardware on the host system. It is using internally dynamic binary translation from target code to host code to simulate the application software. A potential issue with simulators is that they might not accurately simulate the real hardware. We aimed at filling this gap by proving that the ARM instruction set simulator coded in C is a high fidelity implementation of the ARM architecture, using the Coq theorem prover, and starting from a formal architectural model in Coq. The first part of the chapter presents the general architecture and features of SimSoC. The second part describes the proof of the ARM simulator.

Design of real-time MPSoC systems including multiple applications is challenging because temporal requirements of each application must be respected throughout the entire design flow. Currently the design of different applications is often interdependent, making converge to a solution for each application difficult. This chapter proposes a compositional method to design applications independently, and then to execute them without interference. We define a formal modeling framework as a suitable entry point for application design. The models are executable, which enables early detection of specification errors, and include the formal properties of the applications based on well-defined models of computation. We combine this with a predictable MPSoC platform template that has a supporting design flow but lacks a simulation front-end. The structure and behavior of the application models are exported to an intermediate format via introspection which is iteratively transformed for the backend flow. We identify the problems arising in this transformation and provide appropriate solutions. The design flow is demonstrated by a system consisting of two streaming applications where less than half of the design time is dedicated to operating on the integrated system model.

We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and executable code generation. To this end, we use, pState, a tool for the design of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart model, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process or a Probabilistic Timed Automaton. On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of the tag collection to calculate the collision probability and then we use the collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.

The continuous evolution of fabrication technologies has enabled the development of more complex and powerful embedded systems. A related tendency is toward an increasing percentage of the functionality being executed as embedded SW running on the different processors of the Multi-Processing System-on-Chip (MPSoC). In order to reduce the design gap (between design complexity and design productivity) associated with this evolution, the trend is to increase the level of abstraction at which designers and CAD tools work. To deal with this problem, starting the design process from high-level UML models combined with functional codes using (i.e., using C/C++) the different system components has been proposed. Video processing is one of the areas where high-level modeling and analysis based on UML may have a wider impact.

In this chapter, model-driven development (MDD) using UML/MARTE is proposed to support the specification and analysis of a positioning system for “recreated reality” applications. By recreated reality, we mean providing the user with an immersive experience based on synthetic, 3D images combining virtual and real images of the environment where the user is. In this application, a positioning system able to know where the user is at each instant of time is essential.