Abstract
The Model Based Design approach for Hybrid Systems control software synthesis is particularly appealing since Formal System Level Specifications are usually much easier to define than the control software itself. In this setting, Design Space Exploration has the goal to find a suitable (with respect to costs and performance) choice for system design parameters. Unfortunately, a substantial part of the time devoted to design space exploration is spent trying to solve control software synthesis problems that do not have a solution. We present an on-the-fly algorithm to control software synthesis that enables effective design space exploration by speeding-up termination when no controller is found. Our experimental results show the effectiveness of our approach and how it can support a concrete realizability and schedulability analysis.
This work has been partially supported by the the EC FP7 projects GA317761 (SmartHG), GA600773 (PAEON), by MIUR project DM24283 (TRAMP), and by Erasmus Mundus MULTIC scholarship from the European Commission (EMA 2 MULTIC 10-837).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Agrawal, M., Thiagarajan, P.S.: The discrete time behavior of lazy linear hybrid automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 55–69. Springer, Heidelberg (2005)
Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: Automatic control software synthesis for quantized discrete time hybrid systems. In: CDC (2012)
Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: On model based synthesis of embedded control software. In: EMSOFT, pp. 227–236 (2012)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS 138(1), 3–34 (1995)
Alur, R.: Formal verification of hybrid systems. In: EMSOFT, pp. 273–278 (2011)
Basten, T., et al.: Model-driven design-space exploration for embedded systems: The octopus toolset. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol. 6415, pp. 90–105. Springer, Heidelberg (2010)
Bemporad, A.: Hybrid Toolbox (2004), http://cse.lab.imtlucca.it/~bemporad/hybrid/toolbox/
Bemporad, A., Giorgetti, N.: A SAT-based hybrid solver for optimal control of hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 126–141. Springer, Heidelberg (2004)
Benerecetti, M., Faella, M., Minopoli, S.: Revisiting synthesis of switching controllers for linear hybrid systems. In: CDC-ECC, pp. 4753–4758 (2011)
Brogan, W.L.: Modern control theory, 3rd edn. Prentice-Hall, Inc., Upper Saddle River (1991)
Buttazzo, G.C.: Hard Real-Time Computing Systems, 3rd edn. Springer (2011)
Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)
Castiglione, G., Restivo, A., Sciortino, M.: Nondeterministic moore automata and brzozowski’s algorithm. In: Bouchou-Markhoff, B., Caron, P., Champarnaud, J.-M., Maurel, D. (eds.) CIAA 2011. LNCS, vol. 6807, pp. 88–99. Springer, Heidelberg (2011)
Cimatti, A., Roveri, M., Traverso, P.: Strong planning in non-deterministic domains via model checking. In: AIPS, pp. 36–43 (1998)
Easwaran, A., Lee, I., Shin, I., Sokolsky, O.: Compositional schedulability analysis of hierarchical real-time systems. In: ISORC, pp. 274–281 (2007)
Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 456–459. Springer, Heidelberg (1997)
Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 582–593. Springer, Heidelberg (1997)
Holzmann, G.J.: The spin model checker. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Simulink by mathworks, http://www.mathworks.com
Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107–116. ACM (2011)
Kreisselmeier, G., Birkhölzer, T.: Numerical nonlinear regulator design. IEEE Trans. on on Automatic Control 39(1), 33–46 (1994)
Lublinerman, R., Szegedy, C., Tripakis, S.: Modular code generation from synchronous block diagrams: modularity vs. code size. In: POPL, pp. 78–89 (2009)
Majumdar, R., Saha, I., Zamani, M.: Performance-aware scheduler synthesis for control systems. In: EMSOFT 2011, pp. 299–308 (2011)
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Model based synthesis of control software from system level formal specifications. ACM Trans. Softw. Eng. Methodol. (to appear, 2013), A preliminary version is available at http://arxiv.org/pdf/1107.5638v2
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesis of quantized feedback control software for discrete time linear hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 180–195. Springer, Heidelberg (2010)
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Linear constraints as a modeling language for discrete time hybrid systems. In: ICSEA 2012, pp. 664–671 (2012)
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesizing control software from boolean relations. Int. J. on Advances in SW 5(3&4), 212–223 (2012)
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Undecidability of quantized state feedback control for discrete time linear hybrid systems. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 243–258. Springer, Heidelberg (2012)
Mazo Jr., M., Davitian, A., Tabuada, P.: PESSOA: A tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 566–569. Springer, Heidelberg (2010)
Mazo, M., Tabuada, P.: Symbolic approximate time-optimal control. Systems & Control Letters 60(4), 256–263 (2011)
Atmel megaAVR Microcontroller (2013), http://www.atmel.com/products/microcontrollers/avr/megaavr.aspx
Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508–2516 (2008)
Reactis White Paper (2013), http://www.reactive-systems.com/simulink-testing-validation.html
Roy, P., Tabuada, P., Majumdar, R.: Pessoa 2.0: a controller synthesis tool for cyber-physical systems. In: HSCC 2011, pp. 315–316 (2011)
Sontag, E.D.: Mathematical Control Theory: Deterministic Finite Dimensional Systems, 2nd edn. Springer, New York (1998)
Tronci, E.: Automatic synthesis of controllers from formal specifications. In: ICFEM, pp. 134–143. IEEE (1998)
Wong-Toi, H.: The synthesis of controllers for linear hybrid automata. In: CDC, vol. 5, pp. 4607–4612. IEEE (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E. (2013). On-the-Fly Control Software Synthesis. In: Bartocci, E., Ramakrishnan, C.R. (eds) Model Checking Software. SPIN 2013. Lecture Notes in Computer Science, vol 7976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39176-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-39176-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39175-0
Online ISBN: 978-3-642-39176-7
eBook Packages: Computer ScienceComputer Science (R0)