The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.09 - September (2010 vol.59)
pp: 1281-1294
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
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.
INDEX TERMS
Formal languages, software engineering.
CITATION
Madhukar Anand, Sebastian Fischmeister, Yerang Hur, Jesung Kim, Insup Lee, "Generating Reliable Code from Hybrid-Systems Models", IEEE Transactions on Computers, vol.59, no. 9, pp. 1281-1294, September 2010, doi:10.1109/TC.2010.84
REFERENCES
[1] N. Martin, "Lock Who's Talking: Motorola's c.d. Team," LockSmart Online Article, Nov. 1998.
[2] R.N. Charette, "This Car Runs on Code," IEEE Spectrum, Feb. 2009.
[3] R. Alur and D.L. Dill, "A Theory of Timed Automata," Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, Apr. 1994.
[4] R. Alur, F. Ivancic, J. Kim, I. Lee, and O. Sokolsky, "Generating Embedded Software from Hierarchical Hybrid Models," SIGPLAN Notices, vol. 38, no. 7, pp. 171-182, 2003.
[5] D. Harel, "Statecharts: A Visual Formalism for Complex Systems," Science of Computer Programming, vol. 8, pp. 231-274, 1987.
[6] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems," Theoretical Computer Science, vol. 138, pp. 3-34, 1995.
[7] O. Maler, Z. Manna, and A. Pnueli, "From Timed to Hybrid Systems," Proc. Research and Education in Concurrent Systems (REX) Workshop, Real-Time: Theory in Practice, 1991.
[8] F. Ivancic, "Report on Verification of the Mobies Vehicle-Vehicle Automotive Oep Problem," http://citeseer.ist.psu.edu ivancic02report.html , 2002.
[9] Y. Hur, J. Kim, I. Lee, and J.-Y. Choi, "Sound Code Generation from Communicating Hybrid Models," Proc. Int'l Workshop Hybrid Systems: Computation and Control (HSCC), pp. 432-447, 2004.
[10] M. Anand, J. Kim, and I. Lee, "Code Generation from Hybrid Systems Models for Distributed Embedded Systems," Proc. IEEE Int'l Symp. Object-Oriented Real-Time Distributed Computing (ISORC), pp. 166-173, 2005.
[11] M. Anand, S. Fischmeister, J. Kim, and I. Lee, "Distributed-Code Generation from Hybrid Systems Models for Time-Delayed Multirate Systems," Proc. Fifth ACM Int'l Conf. Embedded Software (EMSOFT '05), pp. 210-213, 2005.
[12] R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee, "Modular Specification of Hybrid Systems in CHARON," Proc. Int'l Workshop Hybrid Systems: Computation and Control (HSCC), http:// citeseer.ist.psu.edu/articlealur00modular.html , pp. 6-19, 2000.
[13] P. Traverse, I. Lacaze, and J. Souyris, "Airbus Fly-By-Wire: A Total Approach to Dependability," Proc. IFIP World Congress, pp. 191-212, 2004.
[14] "Rational Rose," IBM, http://www-306.ibm.com/software/ awdtools/ developerrose/, 2010.
[15] TargetLink, http://www.dspaceinc.com/ww/en/inc/home/ products/sw/pcgstargetli.cfm, 2010.
[16] "Simulink," The MathWorks, http://www.mathworks.com/ productssimulink /, 2010.
[17] G. Berry, The Foundations of Esterel. MIT Press, http://citeseer. ist.psu.edu62412.html, 2000.
[18] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The Synchronous Dataflow Programming Language Lustre," Proc. IEEE, vol. 79, no. 9, pp. 1305-1320, Sept. 1991.
[19] N. Halbwachs and P. Raymond, "A Tutorial of Lustre," http://citeseer.ist.psu.eduhalbwachs01tutorial.html , 2009.
[20] A. Deshpande, A. Göllu, and P. Varaiya, "SHIFT: A Formalism and a Programming Language for Dynamic Networks of Hybrid Automata," Hybrid Systems IV, Springer, 1996.
[21] J. Eker, J. Janneck, E. Lee, J. Liu, X. Liu, J. Luvig, S. Neuendorffer, S. Sachs, and Y. Xiong, "Taming Heterogeneity—The Ptolemy Approach," Proc. IEEE, vol. 91, no. 1, pp. 127-144, Jan. 2003.
[22] G. Karsai, J. Sztipanovits, A. Ledeczi, and T. Bapty, "Model-Integrated Development of Embedded Software," Proc. IEEE, vol. 91, no. 1, pp. 145-164, Jan. 2003.
[23] A.R. Girard, A.S. Howell, and J.K. Hedrick, "Model-Driven Hybrid and Embedded Software for Automotive Applications," Proc. Second RTAS Workshop Model-Driven Embedded Systems (MoDES '04), 2004.
[24] B. Shah, R. Dennison, and J. Gray, "A Model-Driven Approach for Generating Embedded Robot Navigation Control Software," Proc. 42nd Ann. Southeast Regional Conf. (ACM-SE 42), pp. 332-335, 2004.
[25] T. Stauner, "Discrete-Time Refinement of Hybrid Automata," Proc. Fifth Int'l Workshop Hybrid Systems: Computation and Control (HSCC '02), pp. 407-420, 2002.
[26] T.A. Henzinger and P.H. Ho, "Algorithmic Analysis of Nonlinear Hybrid Systems," Proc. Seventh Int'l Conf. Computer Aided Verification, P. Wolper, ed., vol. 939, pp. 225-238, http://citeseer.ist. psu.eduhenzinger96algorithmic.html , 1995.
[27] W.H. Press, S.A. Teukolsky, W.T. Vetterling, and B.P. Flannery, Numerical Recipes in C: The Art of Scientific Computing, second ed. Cambridge University Press, 1999.
[28] R. Alur, F. Ivancic, J. Kim, I. Lee, and O. Sokolsky, "Generating Embedded Software from Hierarchical Hybrid Models," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI '03), 2003.
[29] M. Anand, J. Kim, S. Fischmeister, and I. Lee, "Generating Sound and Resource-Aware Code from Hybrid System Models," Model-Driven Development of Reliable Automotive Services, pp. 48-66, 2008.
[30] K.E. Brenan, S.L. Campbell, and L.R. Petzold, Numerical Solution of Initial-Value Problems in Differential-Algebraic Equations, second ed. SIAM, 1996.
[31] Y. Hur, J.-H. Sim, J. Kim, and J.-Y. Choi, "Ensuring Sound Numerical Simulation of Hybrid Automata," J. Computing Science and Eng., vol. 3, no. 2, pp. 73-87, June 2009.
[32] J.-Y. Choi, Y. Hur, and I. Lee, "IHA: Ensuring Sound Numerical Simulation of Hybrid Automata," Technical Report MS-CIS-03-06, Univ. of Pennsylvania, 2003.
[33] J.-Y. Choi, Y. Hur, J. Kim, and I. Lee, "Sound Synchronization of Communicating Hybrid Automata," Technical Report MS-CIS-03-30, Univ. of Pennsylvania, 2003.
[34] A. Fehnker and F. Ivancic, "Benchmarks for Hybrid Systems Verification," Proc. Int'l Workshop Hybrid Systems: Computation and Control (HSCC), pp. 326-341, http://citeseer.ist.psu.edu fehnker04benchmarks.html , 2004.
[35] G.E. Blelloch and M. Reid-Miller, "Fast Set Operations Using Treaps," Proc. 10th Ann. ACM Symp. Parallel Algorithms and Architectures (SPAA '98), pp. 16-26, 1998.
[36] A.A. Julius and G.J. Pappas, "Approximate Equivalence and Approximate Synchronization of Metric Transition Systems," Proc. 44th IEEE Conf. Decision and Control, Dec. 2006.
[37] C. Kossentini and P. Caspi, "Approximation, Sampling and Voting in Hybrid Computing Systems," Proc. Int'l Workshop Hybrid Systems: Computation and Control (HSCC '06), 2006.
25 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool