Generating Reliable Code from Hybrid-Systems Models

Title Generating Reliable Code from Hybrid-Systems Models
Author
Keywords
Abstract

Hybrid systems have emerged as an appropriate formalism to model embedded systems as they capture the theme of continuous dynamics with discrete control. Under this paradigm, distributed embedded systems can be modeled as a network of communicating hybrid automata. Several techniques for code generation from these models have also been proposed and commercially implemented. Providing formal guarantees of the generated code with respect to the model, however, has turned out to be a hard problem. While the model is set in continuous time with concurrent execution and instantaneous switching, the code running on an inherently discrete platform, can be affected by the sampling interval, round-off errors, and communication delays between the sensor, controller, and actuators. Consequently, semantic differences between the model and its code can arise with potentially different system behavior. This paper proposes a criterion for faithful implementation of the hybrid-systems model with a focus on its switching semantics. We discuss different techniques to ensure a faithful implementation of the model, and test the feasibility of our concepts by implementing a model heater system. In this heater case study, we successfully eliminate all fault transitions and, thereby, generate code with correct behavior complying with the specification.

Year of Publication
2010
Journal
IEEE Transactions on Computers
Volume
59
Number of Pages
1281-1294
Date Published
July
ISSN Number
0018-9340
URL
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5453343
DOI
10.1109/TC.2010.84
Download citation