Publicerad: 2011-06-30
ISBN: 978-91-7393-096-3
ISSN: 1650-3686 (tryckt), 1650-3740 (online)
Outputs of synchronous programs may suffer from cyclic dependencies since statements are allowed to read the current outputs’ values to determine the actions that generate the current values of the outputs. For this reason; compilers have to perform a causality analysis that ensures that at any point of time; there is a unique and constructive way to determine the outputs. The discrete parts of hybrid systems may suffer from the same problem as observed in synchronous programs. As we recently extended our synchronous language Quartz to describe hybrid systems; we explain in this paper how the causality analysis as originally introduced for synchronous systems can also be used to handle cyclic dependencies in hybrid Modelica programs.
[1] 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 (TCS) ; 138(1):3–34; 1995.
doi: 10.1016/0304-3975(94)00202-T.
[2] R. Alur; C. Courcoubetis; T. Henzinger; and P.-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R. Grossmann; A. Nerode; A. Ravn; and H. Rischel; editors; Hybrid Systems; volume 736 of LNCS; pages 209–229. Springer; 1993.
[3] R. Alur; T. Henzinger; G. Lafferriere; and G. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE; 88(7):971–984; 2000.
doi: 10.1109/5.871304.
[4] K. Bauer and K. Schneider. From synchronous programs to symbolic representations of hybrid systems. In K. Johansson and W. Yi; editors; Hybrid Systems: Computation and Control (HSCC); pages 41–50; Stockholm; Sweden; 2010. ACM.
[5] K. Bauer and K. Schneider. Predicting events for the simulation of hybrid systems. In International Conference on Embedded Software and Systems (ICESS); Bradford; United Kingdom; 2010. IEEE Computer Society.
[6] A. Benveniste and G. Berry. The synchronous approach to reactive real-time systems. Proceedings of the IEEE; 79(9):1270–1282; 1991.
doi: 10.1109/5.97297.
[7] A. Benveniste; P. Caspi; S. Edwards; N. Halbwachs; P. Le Guernic; and R. de Simone. The synchronous languages twelve years later. Proceedings of the IEEE; 91(1):64–83; 2003.
doi: 10.1109/JPROC.2002.805826.
[8] G. Berry. The foundations of Esterel. In G. Plotkin; C. Stirling; and M. Tofte; editors; Proof; Language and Interaction: Essays in Honour of Robin Milner. MIT Press; 1998.
[9] G. Berry. The constructive semantics of pure Esterel. http://www-sop.inria.fr/esterel.org/; July 1999.
[10] G. Berry. The Esterel v5 language primer. http://www-sop.inria.fr/esterel.org/; July 2000.
[11] G. Berry and G. Gonthier. The Esterel synchronous programming language: Design; semantics; implementation. Science of Computer Programming; 19(2):87–152; 1992.
doi: 10.1016/0167-6423(92)90005-V.
[12] X. Briand and B. Jeannet. Combining control and data abstraction in the verification of hybrid systems. In R. Bloem and P. Schaumont; editors; Formal Methods and Models for Codesign (MEMOCODE); pages 141–150; Cambridge; Massachusetts; USA; 2009. IEEE Computer Society.
[13] D. Campagna and C. Piazza. Hybrid automata in systems biology: How far can we go? Electronic Notes in Theoretical Computer Science (ENTCS); 229:93–108; 2009.
doi: 10.1016/j.entcs.2009.02.007.
[14] L. Carloni; M. Di Benedetto; R. Passerone; A. Pinto; and A. Sangiovanni-Vincentelli. Modeling techniques; programming languages; and design toolsets for hybrid systems; 2004. Report on the Columbus Project; http://www.columbus.gr.
[15] P. Fritzson and V. Engelson. Modelica - a unified object-oriented language for system modeling and simulation. In Object-Oriented Programming; volume 1445 of LNCS; pages 67–90. Springer; 1998.
[16] M. Fränzle. What will be eventually true of polynomial hybrid automata? In N. Kobayashi and B. Pierce; editors; Theoretical Aspects of Computer Software (TACS); volume 2215 of LNCS; pages 340–359; Sendai; Japan; 2001. Springer.
[17] R. Ghosh; A. Tiwari; and C. Tomlin. Automated symbolic reachability analysis with application to delta-notch signaling automata. In O. Maler and A. Pnueli; editors; Hybrid Systems: Computation and Control (HSCC); volume 2623 of LNCS; pages 233–248; Prague; Czech Republic; 2003. Springer.
[18] N. Halbwachs. Synchronous programming of reactive systems. Kluwer; 1993.
doi: 10.1007/978-1-4757-2231-4.
[19] N. Halbwachs; P. Caspi; P. Raymond; and D. Pilaud. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE; 79(9):1305–1320; September 1991.
doi: 10.1109/5.97300.
[20] D. Harel. Statecharts: A visual formulation for complex systems. Science of Computer Programming; 8(3):231–274; 1987.
doi: 10.1016/0167-6423(87)90035-9.
[21] T. Henzinger. The theory of hybrid automata. In Logic in Computer Science (LICS); pages 278–292; New Brunswick; New Jersey; USA; 1996. IEEE Computer Society.
[22] T. Henzinger; P. Kopke; A. Puri; and P. Varaiya. What’s decidable about hybrid automata? In Las Vegas; Nevada; USA ; pages 373–382. ACM; 1995.
[23] G. Lafferriere; G. Pappas; and S. Yovine. A new class of decidable hybrid systems. In F. Vaandrager and J. van Schuppen; editors; Hybrid Systems: Computation and Control (HSCC); volume 1569 of LNCS; pages 137–151; Berg en Dal; The Netherlands; 1999. Springer.
[24] S. Malik. Analysis of cycle combinational circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (T-CAD) ; 13(7):950–956; July 1994.
[25] J. Miller. Decidability and complexity results for timed automata and semi-linear hybrid automata. In N. Lynch and B. Krogh; editors; Hybrid Systems: Computation and Control (HSCC); volume 1790 of LNCS; pages 296–309; Pittsburgh; Pennsylvania; USA; 2000. Springer.
[26] Modelica Association. Modelica - a unified object-oriented language for physical systems modeling; language specification version 2.0; 2002. http://www.Modelica.org.
[27] G. Plotkin. A structural approach to operational semantics. Technical Report FN-19; DAIMI; Aarhus; Denmark; 1981.
[28] S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. In M. Morari and L. Thiele; editors; Hybrid Systems: Computation and Control (HSCC); volume 3414 of LNCS; pages 573–589; Zürich; Switzerland; 2005. Springer.
[29] M. Riedel and J. Bruck. Cyclic combinational circuits: Analysis for synthesis. In International Workshop on Logic and Synthesis (IWLS); Laguna Beach; California; USA; 2003.
[30] M. Riedel and J. Bruck. The synthesis of cyclic combinational circuits. In Design Automation Conference (DAC); pages 163–168; Anaheim; California; USA; 2003. ACM.
[31] K. Schneider. The synchronous programming language Quartz. Internal Report 375; Department of Computer Science; University of Kaiserslautern; Kaiserslautern; Germany; 2009.
[32] K. Schneider and J. Brandt. Performing causality analysis by bounded model checking. In Application of Concurrency to System Design (ACSD); pages 78–87; Xi’an; China; 2008. IEEE Computer Society.
[33] K. Schneider; J. Brandt; T. Schuele; and T. Tuerk. Maximal causality analysis. In J. Desel and Y. Watanabe; editors; Application of Concurrency to System Design (ACSD); pages 106–115; St. Malo; France; 2005. IEEE Computer Society.
[34] T. Shiple; G. Berry; and H. Touati. Constructive analysis of cyclic circuits. In European Design and Test Conference (EDTC); Paris; France; 1996. IEEE Computer Society.
doi: 10.1109/EDTC.1996.494321.
[35] L. Stok. False loops through resource sharing. In International Conference on Computer-Aided Design (ICCAD); pages 345–348. IEEE Computer Society; 1992.
