Scientific publications


Explore the publications from TNO‑ESI, showcasing our research findings and expertise. This includes peer-reviewed articles, conference papers, and research reports, as well as more accessible publications that share insights from our collaborations with industry partners. You can easily search the publications by keyword to find what is most relevant to you.

Year
2010
Authors
Pillai, C.; Fabel, R.; Somers, L.

Model based control software synthesis for paper handling in printers

Control software is an integral part of new complex electromechanical systems, such as professional high speed printers. The development of these multidisciplinary products involves a number of iterative and incremental cycles of prototype creation. Automatically generating control software is a big leap in rapid prototyping of these products.
Year
2010
Authors
Xing, J.; Theelen, B.D.; Langerak, R.; Pol, J. van de; Tretmans, J.; Voeten, J.P.M.

UPPAAL in practice Quantitative verification of a RapidIO network

Packet switched networks are widely used for interconnecting distributed computing platforms. RapidIO (Rapid Input/Output) is an industry standard for packet switched networks to interconnect multiple processor boards. Key performance metrics for these platforms include average-case and worst-case packet transfer latencies.
The design of new embedded systems is getting more and more complex as more functionality is integrated into these systems. To deal with the design complexity, a predictable design flow is needed. The result should be a system that guarantees that an application can perform its own tasks within strict timing deadlines, independent of other applications running on the system.
Year
2010
Authors
Moneva, H.; Vissers, J.

Putting chaos under control On how modeling should support design

Complex systems design faces the lack of seamless integration of model-based methods and techniques. In this paper we propose a framework that enables designers and architects to track the design decisions throughout the design process. It provides a mechanism to deduce the impact of each design decision on the system under design.
Year
2010
Authors
Damavandpeyma, M.; Stuijk, S.; Basten, T.; Geilen, M.; Corporaal, H.

Thermal-aware scratchpad memory design and allocation

Scratchpad memories (SPMs) have become a promising on-chip storage solution for embedded systems from an energy, performance and predictability perspective. The thermal behavior of these types of memories has not been considered in detail. This thermal behavior plays an important role in the reliability of silicon devices and in their static (leakage) power consumption.
Year
2010
Authors
Haverkort, B.R.; Kuntz, M.; Remke, A.; Roolvink, S.

Formal performability evaluation of architectural models of critical infrastructures

In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions.
Year
2010
Authors
Haverkort, B.R.; Kuntz, M.; Leitner-Fischer, F.; Remke, A.; Roolvink, S.

Probabilistic verification of architectural software models using SoftArc and Prism

In this paper we will describe the SoftArc approach. With the SoftArc approach it is possible to model and analyse safety-critical embedded and distributed systems that consist of both hard- and software. We are going to present the SoftArc modelling language, its syntax and semantics. The semantics of the SoftArc modelling language is defined in terms of stochastic reactive modules.
Year
2010
Authors
Li, L.; Hooman, J.; Voeten, J.

Connecting technical and non-technical views of system architectures

When designing, adapting or extending a complex cyber physical system, it extremely difficult to guarantee that all parts cooperate correctly, especially when many parties are involved in the development process. We propose a new approach to identify and to solve problems in the early development phases, thus reducing costs in the system implementation, test and integration phases.
Year
2010
Authors
Jin, L.; Min-Allah, N.; Xing, J.S.; Wang, X.L.

Extended empty-slots method for fixed priority feasibility analysis

For preemptive scheduling, the discrete scheduling has the same capability as the continuous scheduling. However, most work previously done has been focused on the continuous scheduling. In this paper, a discrete analysis approach EmptySlots method is discussed and applied to fixed priority scheduling for constraint-deadline task model.
Year
2010
Authors
Baier, C.; Cloth, L.; Haverkort, B.R.; Hermanns, H.; Katoen, J.-P.

Performability assessment by model checking of Markov reward models

Published in
Formal Methods in System Design, 36(1), pp. 1-36.
This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computercommunication systems.We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures.