![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
Article
Open AccessVisualization, transformation, and analysis of execution traces with the eclipse TRACE4CPS trace tool
An execution trace is a model of a single system behavior. Execution traces occur everywhere in the system’s lifecycle as they can typically be produced by executable models, by prototypes of (sub)systems, and...
-
Article
Open AccessEconomic Crises, Subjective Well-Being, and Vote Switching: The Case of Brazil’s 2018 Presidential Election
This paper examines the influence of the 2015 economic crisis on subjective well-being (SWB) and the withdrawal of support for the incumbent party during the 2018 presidential election in Brazil. Using Gallup ...
-
Article
Open AccessThe influence of CEO compensation on employee engagement
The soaring compensation levels of chief executive officers (CEOs) have spurred an intense debate about its outcomes. This paper examines an understudied outcome in this regard: employee engagement. Using a dy...
-
Article
Open AccessHappy but Unequal: Differences in Subjective Well-Being across Individuals and Space in Colombia
Despite being on average a relatively happy country, Colombia has a high level of inequality in subjective well-being (SWB). Using Gallup World Poll data for the period from 2010 to 2018, this paper tests the ...
-
Chapter
Organizations with Virtuous Leaders Flourish More
This chapter explores the association between virtuous leadership and flourishing in organizations by reviewing the current academic literature. The initial evidence consistently demonstrates that subordinates...
-
Living Reference Work Entry In depth
Happiness and Migration
A subjective well-being angle has emerged as an important new frontier to advance the understanding of the causes and consequences of migration. The purpose of this chapter is to organize and take stock of thi...
-
Article
Open AccessThe joy of lottery play: evidence from a field experiment
Buying lottery tickets is not a rational investment from a financial point of view. Yet, the majority of people participate at least once a year in a lottery. We conducted a field experiment to increase unders...
-
Article
Modeling and Analysis of FPGA Accelerators for Real-Time Streaming Video Processing in the Healthcare Domain
Complex real-time video processing applications with strict throughput constraints are commonly found in a typical healthcare application. The video processing chain is implemented as Field-Programmable Gate A...
-
Article
Open AccessMonotonic Optimization of Dataflow Buffer Sizes
Many high data-rate video-processing applications are subject to a trade-off between throughput and the sizes of buffers in the system (the storage distribution). These applications have strict requirements wi...
-
Article
Analyzing execution traces: critical-path analysis and distance analysis
System designers make trade-offs between metrics of interest such as execution time, functional quality and cost to create a properly balanced system. Execution traces, which are sequences of timestamped start...
-
Chapter
Happiness Insights into Migration Policy and Choice Behavior of Immigrants
A considerable proportion of immigrants and citizens of their host countries are dissatisfied with the outcomes of migration, even though they have objectively benefited of migration. What is the source of thi...
-
Article
A blueprint for system-level performance modeling of software-intensive embedded systems
Exploration of design alternatives and estimation of their key performance metrics such as latency and energy consumption is essential for making the proper design decisions in the early phases of system devel...
-
Article
Why are Locals Happier than Internal Migrants? The Role of Daily Life
Several survey studies have found that internal migrants report lower levels of happiness than locals, even after accounting for socio-economic factors. Traditional global self-ratings reveal that the migrant–loc...
-
Chapter and Conference Paper
Performance Engineering for Industrial Embedded Data-Processing Systems
Performance is a key aspect of many embedded systems, embedded data processing systems in particular. System performance can typically only be measured in the later stages of system development. To avoid expen...
-
Chapter
Model-Driven Design-Space Exploration for Software-Intensive Embedded Systems
The complexity of today’s embedded systems is increasing rapidly. Ever more functionality is realised in software, for reasons of cost and flexibility. This leads to many implementation alternatives that vary ...
-
Chapter and Conference Paper
Model-Driven Design-Space Exploration for Software-Intensive Embedded Systems
Software plays an increasingly important role in modern embedded systems, leading to a rapid increase in design complexity. Model-driven exploration of design alternatives leads to shorter, more predictable de...
-
Chapter and Conference Paper
Model-Driven Design-Space Exploration for Embedded Systems: The Octopus Toolset
The complexity of today’s embedded systems and their development trajectories requires a systematic, model-driven design approach, supported by tooling wherever possible. Only then, development trajectories be...
-
Article
Model checker aided design of a controller for a wafer scanner
For a case-study of a wafer scanner from the semiconductor industry it is shown how model checking techniques can be used to compute (1) a simple yet optimal deadlock avoidance policy, and (2) an infinite sche...
-
Chapter and Conference Paper
Model Checking the Time to Reach Agreement
The timed automaton framework of Alur and Dill is a natural choice for the specification of partially synchronous distributed systems (systems which have only partial information about timing, e.g., only an up...
-
Chapter and Conference Paper
Adding Symmetry Reduction to Uppaal
We describe a prototype extension of the real-time model checking tool Uppaal with symmetry reduction. The symmetric data type scalarset, which is also used in the Murϕ model checker, was added to Uppaal’s syste...