Abstract
Many Control Systems are indeed Software Based Control Systems, i.e. control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of control software.
Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis.
In this paper, we present a Map-Reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as a discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis.
We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 60%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm implemented in QKS.
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
Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1–15. Springer, Heidelberg (2006)
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.: Model based synthesis of control software from system level formal specifications. ACM Trans. on Soft. Eng. and Meth. (to appear)
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Quantized feedback control software synthesis from system level formal specifications. CoRR abs/1107.5638v1 (2011)
Tomlin, C.J., Lygeros, J., Sastry, S.S.: Computing controllers for nonlinear hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 238–255. Springer, Heidelberg (1999)
Dean, J., Ghemawat, S.: Mapreduce: Simplified data processing on large clusters. In: OSDI, pp. 137–150 (2004)
Lin, J., Dyer, C.: Data-Intensive Text Processing with MapReduce. Synthesis Lectures on Human Language Technologies. Morgan & Claypool Publishers (2010)
Pacheco, P.: Parallel Programming with MPI. Morgan Kaufmann (1997)
Rodriguez, M., Fernandez-Miaja, P., Rodriguez, A., Sebastian, J.: A multiple-input digitally controlled buck converter for envelope tracking applications in radiofrequency power amplifiers. IEEE Trans. on Pow. El. 25(2), 369–381 (2010)
Kreisselmeier, G., Birkhölzer, T.: Numerical nonlinear regulator design. IEEE Trans. on Automatic Control 39(1), 33–46 (1994)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers C-35(8), 677–691 (1986)
Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: Automatic control software synthesis for quantized discrete time hybrid systems. In: CDC, pp. 6120–6125. IEEE (2012)
So, W.C., Tse, C., Lee, Y.S.: Development of a fuzzy logic controller for dc/dc converters: design, computer simulation, and experimental evaluation. IEEE Trans. on Power Electronics 11(1), 24–32 (1996)
Kim, W., Gupta, M.S., Wei, G.Y., Brooks, D.M.: Enabling on-chip switching regulators for multi-core processors using current staggering. In: ASGI (2007)
Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: On model based synthesis of embedded control software. In: EMSOFT (2012)
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)
Della Penna, G., Magazzeni, D., Tofani, A., Intrigila, B., Melatti, I., Tronci, E.: Automated Generation of Optimal Controllers through Model Checking Techniques. In: Cetto, J.A., Ferrier, J.-L., Costa dias Pereira, J.M., Filipe, J. (eds.) Informatics in Control Automation and Robotics. LNEE, vol. 15, pp. 107–119. Springer, Heidelberg (2008)
Della Penna, G., Magazzeni, D., Mercorio, F., Intrigila, B.: UPMurphi: A tool for universal planning on pddl+ problems. In: ICAPS (2009)
Mazo, M.J., Tabuada, P.: Symbolic approximate time-optimal control. Systems & Control Letters 60(4), 256–263 (2011)
Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107–116. ACM (2011)
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)
Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers – an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 90–104. Springer, Heidelberg (2009)
Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in eddy. Int. J. Softw. Tools Technol. Transf. 11(1), 13–25 (2009)
Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Legay, A.: Distributed parametric and statistical model checking. In: PDMC, pp. 30–42 (2011)
Barnat, J., Brim, L., Ceska, M., Rockai, P.: Divine: Parallel distributed model checker. In: PDMC. PDMC-HIBI 2010, pp. 4–7. IEEE Computer Society, Washington, DC (2010)
Schubert, W., Stengel, R.: Parallel synthesis of robust control systems. IEEE Trans. on Contr. Sys. Techn. 6(6), 701–706 (1998)
Jurikovič, M., Čičák, P., Jelemenská, K.: Parallel controller design and synthesis. In: Proceedings of the 7th FPGAworld Conference, FPGAworld 2010, pp. 35–40. ACM, New York (2010)
Pardey, J., Amroun, A., Bolton, M., Adamski, M.: Parallel controller synthesis for programmable logic devices. Microprocessors and Microsystems 18(8), 451–457 (1994)
Mari, F., Melatti, I., Salvo, I., Tronci, E.: Linear constraints as a modeling language for discrete time hybrid systems. In: ICSEA. IARIA (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.: Control software visualization. In: INFOCOMP. IARIA (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)
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). A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software. 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_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-39176-7_4
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)