From synchronous programs to symbolic representations of hybrid systems

ABSTRACT

In this paper, we present an extension of the synchronous language Quartz by new kinds of variables, actions and statements for modeling the interaction of synchronous systems with their continuous environment. We present an operational semantics of the obtained hybrid modeling language and moreover show how compilation algorithms that have been originally developed for synchronous languages can be extended to these hybrid programs. Thus, we can automatically translate the hybrid programs to compact symbolic representations of hybrid transition systems that can be immediately used for simulation and formal verification.

References

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.
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 Hybrid Systems, volume 736 of LNCS, pages 209--229. Springer, 1993.
3. R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee. Modular specification of hybrid systems in Charon. In Hybrid Systems: Computation and Control (HSCC), volume 1790 of LNCS, pages 6--19, Pittsburgh, PA, USA, 2000. Springer.
4. R. Alur and T. Henzinger. Modularity for timed and hybrid systems. In Conference on Concurrency Theory (CONCUR), volume 1243 of LNCS, pages 74--88, Warsaw, Poland, 1997. Springer.
5. R. Alur, T. Henzinger, G. Lafferriere, and G. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88(7):971--984, 2000.
6. M. Baldamus and T. Stauner. Modifying Esterel concepts to model hybrid systems. Electronic Notes in Theoretical Computer Science (ENTCS), 65(5), 2002. Workshop on Synchronous Languages, Applications, and Programming (SLAP).
7. S. Basu. An improved algorithm for quantifier elimination over real closed fields. In Foundations of Computer Science (FOCS), pages 56--65, Washington, DC, USA, 1997. IEEE Computer Society.
8. A. Benveniste and G. Berry. The synchronous approach to reactive real-time systems. Proceedings of the IEEE, 79(9):1270--1282, 1991.
9. 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.
10. G. Berry. The foundations of Esterel. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998.
11. G. Berry. The constructive semantics of pure Esterel. http://www-sop.inria.fr/esterel.org, July 1999.
12. G. Berry. The Esterel v5 language primer. http://www-sop.inria.fr/esterel.org, July 2000.
13. G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87--152, 1992.
14. C. Berthet, O. Coudert, and J. Madre. New ideas on symbolic manipulations of finite state machines. In International Conference on Computer Design (ICCD), pages 224--227, Cambridge, MA, USA, 1990. IEEE Computer Society.
15. S. Bornot and J. Sifakis. On the composition of hybrid systems. In Hybrid Systems: Computation and Control (HSCC), volume 1386 of LNCS, pages 49--63, Berkeley, California, USA, 1998. Springer.
16. S. Bornot and J. Sifakis. An algebraic framework for urgency. Information and Computation, 163(1):172--202, 2000.
17. J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 10^20 states and beyond. In Logic in Computer Science (LICS), pages 1--33, Washington, DC, USA, 1990. IEEE Computer Society.
18. 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.
19. 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.
20. L. Carloni, R. Passerone, A. Pinto, and A. Sangiovanni-Vincentelli. Languages and tools for hybrid systems design. Foundations and Trends in Electronic Design Automation, 1(1/2):1--193, 2006.
21. P. Caspi, A. Curic, A. Maignan, C. Sofronis, S. Tripakis, and P. Niebert. From Simulink to Scade/Lustre to TTA: A layered approach for distributed embedded applications. In Languages, Compilers, and Tools for Embedded Systems (LCTES), pages 153--162, San Diego, California, USA, 2003. ACM.
22. E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venter, D. Weil, and S. Yovine. TAXYS: A tool for the development and verification of real-time embedded systems. In Computer Aided Verification (CAV), volume 2102 of LNCS, pages 391--395, Paris, France, 2001. Springer.
23. G. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In H. Barkhage, editor, Automata Theory and Formal Languages, volume 33 of LNCS, pages 134--183, Kaiserslautern, Germany, 1975. Springer.
24. W. Damm, S. Disch, H. Hungar, S. Jacobs, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Exact state set representations in the verification of linear hybrid systems with large discrete state space. In Automated Technology for Verification and Analysis (ATVA), volume 4762 of LNCS, pages 425--440, Tokyo, Japan, 2007. Springer.
25. W. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Automatic verification of hybrid systems with large discrete state space. In International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of LNCS, pages 276--291, Beijing, China, 2006. Springer.
26. A. Deshpande, A. Gollu, and L. Semenzato. The SHIFT programming language for dynamic networks of hybrid automata. IEEE Transactions on Automatic Control, 43(4):584--587, April 1998.
27. G. Frehse. PHAVer: Algorithmic verification of hybrid systems past HyTech. In Hybrid Systems: Computation and Control (HSCC), volume 3414 of LNCS, pages 258--273, Zurich, Switzerland, 2005. Springer.
28. M. Fränzle. What will be eventually true of polynomial hybrid automata? In Theoretical Aspects of Computer Software (TACS), volume 2215 of LNCS, pages 340--359, Sendai, Japan, 2001. Springer.
29. R. Ghosh, A. Tiwari, and C. Tomlin. Automated symbolic reachability analysis with application to delta-notch signaling automata. In Hybrid Systems: Computation and Control (HSCC), volume 2623 of LNCS, pages 233--248, Prague, Czech Republic, 2003. Springer.
30. N. Halbwachs. Synchronous programming of reactive systems. Kluwer, 1993.
31. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305--1320, sep 1991.
32. D. Harel. Statecharts: A visual formulation for complex systems. Science of Computer Programming, 8(3):231--274, 1987.
33. T. Henzinger. The theory of hybrid automata. In Symposium on Logic in Computer Science (LICS), pages 278--292, New Brunswick, New Jersey, 1996.
34. T. Henzinger. Masaccio: A formal model for embedded components. In Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics, volume 1872 of LNCS, pages 549--563, Sendai, Japan, 2000. Springer.
35. T. Henzinger. The symbolic approach to hybrid systems. In Computer Aided Verification (CAV), volume 2404 of LNCS, page 57, Copenhagen, Denmark, 2002. Springer.
36. T. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1019 of LNCS, pages 41--71, Aarhus, Denmark, 1995. Springer.
37. T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Annual ACM Symposium on Theory of Computing, pages 373--382, Las Vegas, USA, 1995. ACM.
38. T. Henzinger and R. Majumdar. Symbolic model checking for rectangular hybrid systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1785 of LNCS, pages 142--156, Berlin, Germany, 2000. Springer.
39. B. Izaias Silva and B. Krogh. Formal verification of hybrid systems using CheckMate: A case study. In American Control Conference, pages 1679--1683, Chicago, Illinois, 2000. IEEE Computer Society.
40. G. Lafferriere, J. Pappas, and S. Yovine. A new class of decidable hybrid systems. In J. v. F.W. Vaandrager, editor, Hybrid Systems: Computation and Control (HSCC), volume 1569 of LNCS, pages 137--151, Berg en Dal, The Netherlands, 1999. Springer.
41. J. Miller. Decidability and complexity results for timed automata and semi-linear hybrid automata. In Hybrid Systems: Computation and Control (HSCC), volume 1790 of LNCS, pages 296--310, Pittsburgh, PA, USA, 2000. Springer.
42. Modelica Association. Modelica - a unified object-oriented language for physical systems modeling, language specification version 2.0, 2002. http://www.Modelica.org.
43. F. Pecheux, C. Lallement, and A. Vachoux. VHDL-AMS and Verilog-AMS as alternative hardware description languages for efficient modeling of multidiscipline systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(2):204--225, February 2009.
44. A. Pinto, L. Carloni, R. Passerone, and A. Sangiovanni-Vincentelli. Interchange format for hybrid systems: Abstract semantics. In Hybrid Systems: Computation and Control (HSCC), volume 3927 of LNCS, pages 491--506, Santa Barbara, CA, USA, 2006. Springer.
45. G. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Aarhus University, 1981.
46. S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. In Hybrid Systems: Computation and Control (HSCC), volume 3414 of LNCS, pages 573--589, Zurich, Switzerland, 2005. Springer.
47. K. Schneider. Verification of Reactive Systems - Formal Methods and Algorithms. Texts in Theoretical Computer Science (EATCS Series). Springer, 2003.
48. K. Schneider. The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, 2009.
49. F. Torrisi and A. Bemporad. HYSDEL - a tool for generating computational hybrid models for analysis and synthesis problems. IEEE Transactions on Control Systems Technology, 12(2):235--249, 2004.
50. A. Vachoux, C. Grimm, and K. Einwich. Analog and mixed signal modelling with SystemC-AMS. In International Symposium on Circuits and Systems (ISCAS), pages 914--917. IEEE Computer Society, 2003.
51. D. Walter, S. Little, C. Myers, N. Seegmiller, and T. Yoneda. Verification of analog/mixed-signal circuits using symbolic methods. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 27(12):2223--2235, December 2008.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

• Theory of computation

  • Formal languages and automata theory

  • Logic

  • Semantics and reasoning

    • Program reasoning