Showing 1–6 of 6 results for author: Cauchi, N

Analyzing Occupancy-Driven Thermal Dynamics in Smart Buildings

Authors: Khaza Anuarul Hoque, Nathalie Cauchi, Alessandro Abate

Abstract: The fact that a proper HVAC control strategy can reduce the energy consumption of a building by up to 45% has driven significant research in demand-based HVAC control. This paper presents a novel framework for modeling and analysis of thermal dynamics in smart buildings that incorporates building's thermal properties, a stochastic occupancy model and heating strategies. Each zone of a building is… ▽ More The fact that a proper HVAC control strategy can reduce the energy consumption of a building by up to 45% has driven significant research in demand-based HVAC control. This paper presents a novel framework for modeling and analysis of thermal dynamics in smart buildings that incorporates building's thermal properties, a stochastic occupancy model and heating strategies. Each zone of a building is modeled with the help of discrete time Markov rewards formalism where the states represent the occupancy of that zone (either occupied or empty), and the state rewards incorporate the thermal dynamics and heating strategy. To demonstrate the applicability of our proposed framework, we evaluate and compare six different heating strategies for the two zone scenario of a university building. The obtained quantitative results from the PRISM probabilistic model checker show that one of the evaluated control strategies (viz. selective strategy) satisfies our requirement in terms of maintaining the occupants' comfort while being up to 13.5 times more cost effective when compared to the other evaluated strategies. Such evaluations demonstrate the framework's ability to assist in selecting the control strategy tailored around the occupancy pattern and building's thermal property. △ Less

Submitted 14 March, 2019; originally announced March 2019.

Comments: extended version

StocHy: automated verification and synthesis of stochastic processes

Authors: Nathalie Cauchi, Kurt Degiorgio, Alessandro Abate

Abstract: StocHy is a software tool for the quantitative analysis of discrete-time stochastic hybrid systems (SHS). StocHy accepts a high-level description of stochastic models and constructs an equivalent SHS model. The tool allows to (i) simulate the SHS evolution over a given time horizon; and to automatically construct formal abstractions of the SHS. Abstractions are then employed for (ii) formal verifi… ▽ More StocHy is a software tool for the quantitative analysis of discrete-time stochastic hybrid systems (SHS). StocHy accepts a high-level description of stochastic models and constructs an equivalent SHS model. The tool allows to (i) simulate the SHS evolution over a given time horizon; and to automatically construct formal abstractions of the SHS. Abstractions are then employed for (ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy allows for modular modelling, and has separate simulation, verification and synthesis engines, which are implemented as independent libraries. This allows for libraries to be easily used and for extensions to be easily built. The tool is implemented in C++ and employs manipulations based on vector calculus, the use of sparse matrices, the symbolic construction of probabilistic kernels, and multi-threading. Experiments show StocHy's markedly improved performance when compared to existing abstraction-based approaches: in particular, StocHy beats state-of-the-art tools in terms of precision (abstraction error) and computational effort, and finally attains scalability to large-sized models (12 continuous dimensions). StocHy is available at www.gitlab.com/natchi92/StocHy. △ Less

Submitted 29 January, 2019; originally announced January 2019.

Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems

Authors: Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, Luca Cardelli

Abstract: This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process… ▽ More This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both finite- and infinite-horizon specifications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables. △ Less

Submitted 6 January, 2019; originally announced January 2019.

Maintenance of Smart Buildings using Fault Trees

Authors: Nathalie Cauchi, Khaza Anuarul Hoque, Marielle Stoelinga, Alessandro Abate

Abstract: Timely maintenance is an important means of increasing system dependability and life span. Fault Maintenance trees (FMTs) are an innovative framework incorporating both maintenance strategies and degradation models and serve as a good planning platform for balancing total costs (operational and maintenance) with dependability of a system. In this work, we apply the FMT formalism to a {Smart Buildi… ▽ More Timely maintenance is an important means of increasing system dependability and life span. Fault Maintenance trees (FMTs) are an innovative framework incorporating both maintenance strategies and degradation models and serve as a good planning platform for balancing total costs (operational and maintenance) with dependability of a system. In this work, we apply the FMT formalism to a {Smart Building} application and propose a framework that efficiently encodes the FMT into Continuous Time Markov Chains. This allows us to obtain system dependability metrics such as system reliability and mean time to failure, as well as costs of maintenance and failures over time, for different maintenance policies. We illustrate the pertinence of our approach by evaluating various dependability metrics and maintenance strategies of a Heating, Ventilation and Air-Conditioning system. △ Less

Submitted 22 June, 2018; v1 submitted 13 June, 2018; originally announced June 2018.

Comments: arXiv admin note: substantial text overlap with arXiv:1801.04263

Benchmarks for cyber-physical systems: A modular model library for building automation systems (Extended version)

Authors: Nathalie Cauchi, Alessandro Abate

Abstract: Building Automation Systems (BAS) are exemplars of Cyber-Physical Systems (CPS), incorporating digital control architectures over underlying continuous physical processes. We provide a modular model library for BAS drawn from expertise developed on a real BAS setup. The library allows to build models comprising of either physical quantities or digital control modules.% which are composable. The st… ▽ More Building Automation Systems (BAS) are exemplars of Cyber-Physical Systems (CPS), incorporating digital control architectures over underlying continuous physical processes. We provide a modular model library for BAS drawn from expertise developed on a real BAS setup. The library allows to build models comprising of either physical quantities or digital control modules.% which are composable. The structure, operation, and dynamics of the model can be complex, incorporating (i) stochasticity, (ii) non-linearities, (iii) numerous continuous variables or discrete states, (iv) various input and output signals, and (v) a large number of possible discrete configurations. The modular composition of BAS components can generate useful CPS benchmarks. We display this use by means of three realistic case studies, where corresponding models are built and engaged with different analysis goals. The benchmarks, the model library and data collected from the BAS setup at the University of Oxford, are kept on-line at https://github.com/natchi92/BASBenchmarks. △ Less

Submitted 17 April, 2018; v1 submitted 16 March, 2018; originally announced March 2018.

Comments: Extension of ADHS conference paper

Efficient Probabilistic Model Checking of Smart Building Maintenance using Fault Maintenance Trees

Authors: Nathalie Cauchi, Khaza Anuarul Hoque, Alessandro Abate, Marielle Stoelinga

Abstract: Cyber-physical systems, like Smart Buildings and power plants, have to meet high standards, both in terms of reliability and availability. Such metrics are typically evaluated using Fault trees (FTs) and do not consider maintenance strategies which can significantly improve lifespan and reliability. Fault Maintenance trees (FMTs) -- an extension of FTs that also incorporate maintenance and degrada… ▽ More Cyber-physical systems, like Smart Buildings and power plants, have to meet high standards, both in terms of reliability and availability. Such metrics are typically evaluated using Fault trees (FTs) and do not consider maintenance strategies which can significantly improve lifespan and reliability. Fault Maintenance trees (FMTs) -- an extension of FTs that also incorporate maintenance and degradation models, are a novel technique that serve as a good planning platform for balancing total costs and dependability of a system. In this work, we apply the FMT formalism to a Smart Building application. We propose a framework for modelling FMTs using probabilistic model checking and present an algorithm for performing abstraction of the FMT in order to reduce the size of its equivalent Continuous Time Markov Chain. This allows us to apply the probabilistic model checking more efficiently. We demonstrate the applicability of our proposed approach by evaluating various dependability metrics and maintenance strategies of a Heating, Ventilation and Air-Conditioning system's FMT. △ Less

Submitted 12 January, 2018; originally announced January 2018.

Comments: conference