A Rewriting-Logic-Based Technique for Modeling Thermal Systems

TL;DR

This paper introduces a formal modeling framework based on rewriting logic for thermal systems, enabling simulation and analysis of physical interactions and heat transfer using Real-Time Maude, supported by case studies.

Contribution

It provides a novel approach to model physical systems as first-class entities and demonstrates how to simulate and verify thermal systems within a formal rewriting logic framework.

Findings

Effective modeling of heat transfer in thermal systems

Implementation of continuous behaviors in Real-Time Maude

Successful case studies demonstrating simulation and model checking

Abstract

This paper presents a rewriting-logic-based modeling and analysis technique for physical systems, with focus on thermal systems. The contributions of this paper can be summarized as follows: (i) providing a framework for modeling and executing physical systems, where both the physical components and their physical interactions are treated as first-class citizens; (ii) showing how heat transfer problems in thermal systems can be modeled in Real-Time Maude; (iii) giving the implementation in Real-Time Maude of a basic numerical technique for executing continuous behaviors in object-oriented hybrid systems; and (iv) illustrating these techniques with a set of incremental case studies using realistic physical parameters, with examples of simulation and model checking analyses.