Federico Mari
Skip Abstract Section
Abstract
Many embedded systems are indeed software-based control systems, that is, 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 embedded systems control software. We present an algorithm, along with a tool QKS implementing it, that from a formal model (as a discrete-time linear hybrid system) of the controlled system (plant), implementation specifications (that is, number of bits in the Analog-to-Digital, AD, conversion) and system-level formal specifications (that is, safety and liveness requirements for the closed loop system) returns correct-by-construction control software that has a Worst-Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. We show feasibility of our approach by presenting experimental results on using it to synthesize control software for a buck DC-DC converter, a widely used mixed-mode analog circuit, and for the inverted pendulum.
- M. Agrawal, F. Stephan, P. S. Thiagarajan, and S. Yang. 2006. Behavioural approximations forrestricted linear differential hybrid automata. In Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control (HSCC'06). J. P. Hespanha and A. Tiwari, Eds., Lecture Notes in Computer Science, vol. 3927, Springer, 4--18. Google Scholar
Digital Library
- M. Agrawal and P. S. Thiagarajan. 2005. The discrete time behavior of lazy linear hybrid automata. In Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC'05). M. Morari and L. Thiele, Eds., Lecture Notes in Computer Science, vol. 3414, Springer, 55--69. Google ScholarDigital Library
- V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012a. Automatic control software synthesis for quantized discrete time hybrid systems. In Proceedings of the Conference on Decision and Control (CDC'12). To appear. (A preliminary version can be found at http://arxiv.org/abs/1207.4098.)Google Scholar
- V. Alimguzhin, F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012b. On model based synthesis of embedded control software. In Proceedings of the International Conference on Embedded Software (EMSOFT'12). To appear. Google ScholarDigital Library
- R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. 1995. The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 1, 3--34. Google ScholarDigital Library
- R. Alur, T. Dang, and F. Ivančić. 2006. Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5, 1, 152--199. Google ScholarDigital Library
- R. Alur, T. Henzinger, G. Lafferriere, and G. Pappas. 2000. Discrete abstractions of hybrid systems. Proc. IEEE 88, 7, 971--984.Google ScholarCross Ref
- R. Alur, T. A. Henzinger, and P.-H. Ho. 1996. Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Engin. 22, 3, 181--201. Google ScholarDigital Library
- R. Alur and P. Madhusudan. 2004. Decision problems for timed automata: A survey. In Proceedings of the International School on Formal Methods for the Design of Computer Communication. Lecture Notes in Computer Science, vol. 3185, Springer, 1--24.Google ScholarCross Ref
- E. Asarin and O. Maler. 1999. As soon as possible: Time optimal control for timed automata. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control (HSCC'99). Lecture Notes in Computer Science, vol. 1569, Springer, 19--30. Google ScholarDigital Library
- P. C. Attie, A. Arora, and E. A. Emerson. 2004. Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst. 26, 1, 125--185. Google ScholarDigital Library
- A. Bemporad. 2004. Hybrid toolbox. http://cse.lab.imtlucca.it/∼bemporad/hybrid/toolbox/.Google Scholar
- A. Bemporad and N. Giorgetti. 2004. A sat-based hybrid solver for optimal control of hybrid systems. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04). Lecture Notes in Computer Science, vol. 2993, Springer, 126--141.Google Scholar
- M. Benerecetti, M. Faella, and S. Minopoli. 2011. Revisiting synthesis of switching controllers for linear hybrid systems. In Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'11). 4753--4758.Google Scholar
- W. L. Brogan. 1991. Modern Control Theory 3rd Ed. Prentice-Hall, Upper Saddle River, NJ. Google ScholarDigital Library
- R. Bryant. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35, 8, 677--691. Google ScholarDigital Library
- F. Cassez, A. David, E. Fleury, K. G. Larsen, and D. Lime. 2005. Efficient on-the-fly algorithms for the analysis of timed games. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05). Lecture Notes in Computer Science, vol. 3653, Springer, 66--80. Google ScholarDigital Library
- P. Cerný, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh. 2011. Quantitative synthesis for concurrent programs. In Computer Aided Verification, G. Gopalakrishnan and S. Qadeer, Eds., Springer, 243--259. Google ScholarDigital Library
- A. Cimatti, M. Roveri, and P. Traverso. 1998. Strong planning in non-deterministic domains via model checking. In Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems (AIPS'98). 36--43.Google Scholar
- G. Della Penna, D. Magazzeni, F. Mercorio, and B. Intrigila. 2009. UPMurphi: A tool for universal planning on pddl+ problems. In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS'09). 106--113.Google Scholar
- G. Della Penna, D. Magazzeni, A. Tofani, B. Intrigila, I. Melatti, and E. Tronci. 2008. Automated Generation of Optimal Controllers through Model Checking Techniques. Lecture Notes in Electrical Engineering, vol. 15, Springer.Google Scholar
- A. Dominguez-Garcia and P. Krein. 2008. Integrating reliability into the design of fault-tolerant power electronics systems. In Proceedings of the IEEE Power Electronics Specialists Conference (PESC'08). 2665--2671.Google Scholar
- J. Eker, J. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Sachs, and Y. Xiong. 2003. Taming heterogeneity - The ptolemy approach. Proc. IEEE 91, 1, 127--144.Google ScholarCross Ref
- G. Frehse. 2008. Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transf. 10, 3, 263--279. Google ScholarDigital Library
- M. Fu and L. Xie. 2005. The sector bound approach to quantized feedback control. IEEE Trans. Autom. Control 50, 11, 1698--1711.Google ScholarCross Ref
- A. Girard, G. Pola, and P. Tabuada. 2010. Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55, 1, 116--126.Google ScholarCross Ref
- A. Girault and É Rutten. 2009. Automating the addition of fault tolerance with discrete controller synthesis. Formal Methods Syst. Des. 35, 2, 190--225. Google ScholarDigital Library
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. 2011. Synthesis of loop-free programs. In Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI'11). M. W. Hall and D. A. Padua, Eds., 62--73. Google ScholarDigital Library
- T. Gvero, V. Kuncak, and R. Piskac. 2011. Interactive synthesis of code snippets. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). G. Gopalakrishnan and S. Qadeer, Eds., Lecture Notes in Computer Science, vol. 6806, Springer, 418--423. Google ScholarDigital Library
- T. Henzinger, P.-H. Ho, and H. Wong-Toi. 1997. Hytech: A model checker for hybrid systems. Softw. Tools Technol. Transfer 1, 1, 110--122.Google ScholarDigital Library
- T. A. Henzinger. 2010. From boolean to quantitative notions of correctness. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10). ACM Press, New York, 157--158. Google ScholarDigital Library
- T. A. Henzinger and P. W. Kopke. 1997. Discrete-time control for rectangular hybrid automata. In Proceedings of the 24th Colloquium on Automata, Languages, and Programming (ICALP'97). 582--593. Google ScholarDigital Library
- T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. 1998. What's decidable about hybrid automata? J. Comput. Syst. Sci. 57, 1, 94--124. Google ScholarDigital Library
- T. A. Henzinger and J. Sifakis. 2006. The embedded systems design challenge. In Proceedings of the 14th International Symposium on Formal Methods (FM'06). Lecture Notes in Computer Science, vol. 4085, Springer, 1--15. Google ScholarDigital Library
- H. Hermanns, K. G. Larsen, J.-F. Raskin, and J. Tretmans. 2010. Quantitative system validation in model driven design. In Proceedings of the 8th ACM International Conference on Embedded Software (EMSOFT'10). ACM Press, New York, 301--302. Google ScholarDigital Library
- S. Jha, S. A. Seshia, and A. Tiwari. 2011. Synthesis of optimal switching logic for hybrid systems. In Proceedings of the 9th ACM International Conference on Embedded Software (EMSOFT'11). ACM Press, New York, 107--116. Google ScholarDigital Library
- S. K. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari. 2010. Synthesizing switching logic for safety and dwell-time requirements. Tech. rep. UCB/EECS-2010-28, EECS Department, University of California, Berkeley.Google Scholar
- W. Kim, M. S. Gupta, G.-Y. Wei, and D. M. Brooks. 2007. Enabling on-chip switching regulators for multi-core processors using current staggering. In Proceedings of the Workshop on Architectural Support for Gigascale Integration (ASGI'07).Google Scholar
- G. Kreisselmeier and T. Birkhölzer. 1994. Numerical nonlinear regulator design. IEEE Trans. Autom. Control 39, 1, 33--46.Google ScholarCross Ref
- V. Kuncak, M. Mayer, R. Piskac, and P. Suter. 2010. Comfusy: A tool for complete functional synthesis. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV'10), T. Touili, B. Cook, and P. Jackson, Eds., Lecture Notes in Computer Science, vol. 6174, Springer, 430--433. Google ScholarDigital Library
- V. Kuncak, M. Mayer, R. Piskac, and P. Suter. 2012. Software synthesis procedures. Comm. ACM 55, 2, 103--111. Google ScholarDigital Library
- K. G. Larsen, P. Pettersson, and W. Yi. 1997. Uppaal: Status and developments. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97). Lecture Notes in Computer Science, vol. 1254, Springer, 456--459. Google ScholarDigital Library
- O. Maler, Z. Manna, and A. Pnueli. 1992. From timed to hybrid systems. In Proceedings of the REX Workshop on Real-Time: Theory in Practice. J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, Eds., Lecture Notes in Computer Science, vol. 600, Springer, 447--484. Google ScholarDigital Library
- O. Maler, D. Nickovic, and A. Pnueli. 2007. On synthesizing controllers from bounded-response properties. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Lecture Notes in Computer Science, vol. 4590, Springer, 95--107. Google ScholarDigital Library
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2010. Synthesis of quantized feedback control software for discrete time linear hybrid systems. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV'10). Lecture Notes in Computer Science, vol. 6174, 180--195. Google ScholarDigital Library
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2011a. From boolean relations to control software. In Proceedings of the 6th International Conference on Software Engineering Advances (ICSEA'11).Google Scholar
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2011b. Quantized feedback control software synthesis from system level formal specifications. CoRR abs/1107.5638v1.Google Scholar
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2011c. Quantized feedback control software synthesis from system level formal specifications for buck dc/dc converters. CoRR abs/1105.5640. http://arxiv.org/pdf/1105.5640.pdf.Google Scholar
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012a. Control software visualization. In Proceedings of the 2nd International Conference on Advanced Communications and Computation (INFOCOMP'12). ThinkMind, 15--20.Google Scholar
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012b. Linear constraints as a modeling language for discrete time hybrid systems. In Proceedings of the 7th International Conference on Software Engineering Advances. ThinkMind, 664--671.Google Scholar
- F. Mari, I. Melatti, I. Salvo, and E. Tronci. 2012c. Undecidability of quantized state feedback control for discrete time linear hybrid systems. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC'12). A. Roychoudhury and M. D'Souza, Eds., Lecture Notes in Computer Science, vol. 7521, Springer, 243--258. Google ScholarDigital Library
- M. Mazo, A. Davitian, and P. Tabuada. 2010. Pessoa: A tool for embedded controller synthesis. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV'10). Lecture Notes in Computer Science, vol. 6174, Springer, 566--569. Google ScholarDigital Library
- M. J. Mazo and P. Tabuada. 2011. Symbolic approximate time-optimal control. Syst. Control Lett. 60, 4, 256--263.Google ScholarCross Ref
- D. Monniaux. 2010. Quantifier elimination by lazy model enumeration. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV'10). Lecture Notes Computer Science, vol. 6174, Springer, 585--599. Google ScholarDigital Library
- A. Neumaier and O. Shcherbina. 2004. Safe bounds in linear and mixed-integer programming. Math. Program. Ser. A 99, 283--296. Google ScholarDigital Library
- H.-J. Peter, R. Ehlers, and R. Mattmüller. 2011. Synthia: Verification and synthesis for timed automata. In Computer Aided Verification. G. Gopalakrishnan and S. Qadeer, Eds., Springer, 649--655. Google ScholarDigital Library
- A. Platzer and E. M. Clarke. 2009. Formal verification of curved flight collision avoidance maneuvers: A case study. In Proceedings of the 2nd World Congress on Formal Methods (FM'09). A. Cavalcanti and D. Dams, Eds., Lecture Notes in Computer Science, vol. 5850, Springer, 547--562. Google ScholarDigital Library
- A. Pnueli and R. Rosner. 1989a. On the synthesis of a reactive module. In Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages (POPL'89). ACM Press, New York, 179--190. Google ScholarDigital Library
- A. Pnueli and R. Rosner. 1989b. On the synthesis of an asynchronous reactive module. In Proceedings of the Conference on Automata, Languages and Programming (ICALP'89). G. Ausiello, M. Dezani-Ciancaglini, and S. R. D. Rocca, Eds., Lecture Notes in Computer Science, vol. 372, Springer, 652--671. Google ScholarDigital Library
- G. Pola, A. Girard, and P. Tabuada. 2007. Symbolic models for nonlinear control systems using approximate bisimulation. In Proceedings of the 46th IEEE Conference on Decision and Control. 4656--4661.Google Scholar
- QKS Web Page. 2011. http://mclab.di.uniroma1.it/.Google Scholar
- P. J. Ramadge and W. M. Wonham. 1987. Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25, 1, 206--230. Google ScholarDigital Library
- S. Sankaranarayanan and A. Tiwari. 2011. Relational abstractions for continuous and hybrid systems. In Computer Aided Verification. G. Gopalakrishnan and S. Qadeer, Eds., Springer, 686--702. Google ScholarDigital Library
- SCADE Web Page. 2012. http://www.esterel-technologies.com/products/scade-system/.Google Scholar
- S. Schewe and B. Finkbeiner. 2006. Synthesis of asynchronous systems. In Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). G. Puebla, Ed., Lecture Notes in Computer Science Series, vol. 4407, Springer, 127--142. Google ScholarDigital Library
- G. Schrom, P. Hazucha, J. Hahn, D. Gardner, B. Bloechel, G. Dermer, S. Narendra, T. Karnik, and V. De. 2004. A 480-mhz, multi-phase interleaved buck dc-dc converter with hysteretic control. In Proceedings of the 35th Annual IEEE Power Electronics Specialist Conference (PESC'04). 4702--4707.Google Scholar
- Simulink Web Page. 2012. http://www.mathworks.it/products/simulink/.Google Scholar
- W.-C. So, C. Tse, and Y.-S. Lee. 1996. Development of a fuzzy logic controller for dc/dc converters: Design, computer simulation, and experimental evaluation. IEEE Trans. Power Electron. 11, 1, 24--32.Google ScholarCross Ref
- S. Srivastava, S. Gulwani, S. Chaudhuri, and J. S. Foster. 2011. Path-based inductive synthesis for program inversion. In Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI'11). M. W. Hall and D. A. Padua, Eds., ACM Press, New York, 492--503. Google ScholarDigital Library
- S. Srivastava, S. Gulwani, and J. S. Foster. 2010. From program verification to program synthesis. In Proceedings of the 37th Symposium on Principles of Programming Languages (POPL'10). M. V. Hermenegildo and J. Palsberg, Eds., ACM Press, New York, 313--326. Google ScholarDigital Library
- A. Taly, S. Gulwani, and A. Tiwari. 2009. Synthesizing switching logic using constraint solving. In Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09). Lecture Notes in Computer Science, vol. 5403, Springer, 305--319. Google ScholarDigital Library
- Texas Instruments. 2001. Slvp182: High accuracy synchronous buck dc-dc converter. http://focus.ti.com.cn/cn/lit/ug/slvu046/slvu046.pdf.Google Scholar
- A. Tiwari. 2008. Abstractions for hybrid systems. Formal Methods Syst. Des. 32, 1, 57--83. Google ScholarDigital Library
- E. Tronci. 1996. Optimal finite state supervisory control. In Proceedings of the 35th IEEE Conference on Decision and Control (CDC'96).Google ScholarCross Ref
- E. Tronci. 1997. On computing optimal controllers for finite state systems. In Proceedings of the 36th IEEE Conference on Decision and Control (CDC'97). Vol. 4, 3592--3593Google ScholarCross Ref
- E. Tronci. 1998. Automatic synthesis of controllers from formal specifications. In Proceedings of the 2nd International Conference on Formal Engineering Methods (ICFEM'98). 134--143. Google ScholarDigital Library
- E. Tronci. 1999a. Automatic synthesis of control software for an industrial automation control system. In Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ASE'99). 247--250. Google ScholarDigital Library
- E. Tronci. 1999b. Formally modeling a metal processing plant and its closed loop specifications. In Proceedings of the 4th IEEE International Symposium on High Assurance Systems Engineering (HASE'99). 151--158. Google ScholarDigital Library
- H. Wong-Toi. 1997. The synthesis of controllers for linear hybrid automata. In Proceedings of the 36th IEEE Conference on Decision and Control (CDC'97). Vol. 5, 4607--4612Google ScholarCross Ref
- V. Yousefzadeh, A. Babazadeh, B. Ramachandran, E. Alarcon, L. Pao, and D. Maksimovic. 2008. Proximate time-optimal digital control for synchronous buck dc--dc converters. IEEE Trans. Power Electron. 23, 4, 2018--2026.Google ScholarCross Ref
Index Terms
- Model-based synthesis of control software from system-level formal specifications
Recommendations
Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications
HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and ControlWe address the problem of diagnosing and repairing specifications for hybrid systems, formalized in signal temporal logic (STL). Our focus is on automatic synthesis of controllers from specifications using model predictive control. We build on recent ...
Automatic Synthesis of Control Software for an Industrial Automation Control System
ASE '99: Proceedings of the 14th IEEE international conference on Automated software engineeringWe present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller ...
On model based synthesis of embedded control software
EMSOFT '12: Proceedings of the tenth ACM international conference on Embedded softwareMany Embedded Systems are indeed Software Based Control Systems (SBCSs), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for ...
Comments