Issue No. 09 - September (2010 vol. 59)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2010.84
Madhukar Anand , Cisco Systems
Sebastian Fischmeister , University of Waterloo, Canada
Yerang Hur , Postdata America R & D Center
Jesung Kim , The MathWorks
Insup Lee , University of Pennsylvania, Philadelphia
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.
Formal languages, software engineering.
J. Kim, M. Anand, Y. Hur, S. Fischmeister and I. Lee, "Generating Reliable Code from Hybrid-Systems Models," in IEEE Transactions on Computers, vol. 59, no. , pp. 1281-1294, 2010.