The temporal correctness of safety-critical systems is typically guaranteed via a response-time analysis, whose goal is to determine the worst-case response time (WCRT) of a set of input jobs when they are scheduled by a given scheduling policy on a computing resource. However, response-time analysis is a hard problem to solve, with most variations of the problem being NP-hard. Recently, Nasri et al. have introduced an exact reachability-based response-time analysis that is based on exploring the space of possible decisions that a scheduler can take for a set of jobs/tasks. Their solution is at least three orders of magnitude faster than other exact response-time analyses and scales well. Despite its current success in scalability, the schedule-abstraction-based analysis still faces one big fundamental limitation: in the reachability graph that it builds, each edge can only include one single scheduling decision. As a result, as soon as there are large uncertainties in the release time or execution time of the jobs in the input job set, the number of states generated by the schedule-abstraction graph grows exponentially because the analysis will try to explore all (valid) combinations of ordering between jobs. We improve the scalability of the schedule-abstraction-based analysis by introducing partial-order reduction (POR) rules that allow combining multiple scheduling decisions on one edge and hence avoiding combinatorial exploration of all possible orderings between jobs in cases where there are large uncertainties. Our solution is an exact schedulability analysis and provides a safe response-time analysis that reduces the size of the graph while only introducing a small overestimation on the WCRT of the jobs. Our key idea is to identify subsets of jobs for which the combinatorial exploration of all orderings is irrelevant to the schedulability of the job set. Exploring these combinations is irrelevant when all scenarios lead to a system state without encountering a deadline miss in any of those scenarios. Dispatching such jobs can be considered in a single step (that combines all those scheduling decisions), which further defers the state-space explosion. We show that our solution is able to reduce the runtime of the analysis by five orders of magnitude on average, and the number of explored states by 98% on average in comparison to the original schedule-abstraction-based analysis of Nasri et al. for randomly generated periodic task sets. This achievement comes with a negligible cost of an average 0.1% increase in the WCRT of the jobs. This shows that POR allows us to analyze even more task sets than the original and has the potential to scale even further.

Sick Building Syndrome is present in 30% of all office buildings and can cause serious health damage over time. This is an era where sustainability and well-being are becoming dominant aspects of life. As a result, it is becoming increasingly important to businesses to invest in their employees' well-being and health. The VTTI group cares for the well-being of their employees, and is looking for a tool to optimize the utilization of their building for perceived thermal comfort and indoor air quality. This report documents the development of Claire, an indoor air quality dashboard that helps to identify local air quality problems. Using Claire, employees can be rearranged throughout the space, learn about the characteristics of their office, and for example switch to another meeting room. Claire translates measurements into insights. Claire learns about the behavior of the office, and gives recommendations once she notices that the indoor air quality can be improved. Claire is backed by an indoor air quality sensor mesh network, which has been developed as part of this project. The sensors continuously measure temperature, humidity and carbon dioxide concentrations. The sensors connect to a cloud infrastructure through a local internet gateway. In the cloud the data gets processed. All measurements are displayed real-time in the dashboard. Claire is different from existing products in several ways. First, the sensors developed measure both dry-bulb and black globe temperature, which gives it a temperature reading that describes human thermal comfort more accurately. This is not done in competing products. Furthermore, the sensors fill the gap for small and medium-sized enterprises (SMEs): the sensor network is able to get fine-grained results due to its high sensor density, whilst still being very easy to setup with no adjustments to the building being required. Finally, the developed data analysis methods translate the measurements from the sensor network to concrete suggestions, sent through a push notification, which enables workers to get involved with improving the indoor air quality in their office space.