publication . Preprint . Conference object . 2012

On Model Based Synthesis of Embedded Control Software

Vadim Alimguzhin; Federico Mari; Igor Melatti; Ivano Salvo; Enrico Tronci;
Open Access English
  • Published: 17 Jul 2012
Abstract
Many 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 control software. Given the formal model of a plant as a Discrete Time Linear Hybrid System and the implementation specifications (that is, number of bits in the Analog-to-Digital (AD) conversion) correct-by-construction control software can be automatically generated from System Level Formal Specifications of the closed loop system (that is, safety and liveness requirements), by computing a suitable finite abstra...
Subjects
free text keywords: Computer Science - Software Engineering, Computer Science - Systems and Control, D.2.2, D.2.4, Software requirements specification, Software sizing, Software system, Computer science, Real-time Control System Software, Software verification, Software design, Distributed computing, Real-time computing, Avionics software, Embedded system, business.industry, business, Software construction
Funded by
EC| ULISSE
Project
ULISSE
The USOCs KnowLedge Integration and dissemination for Space Science Experimentation
  • Funder: European Commission (EC)
  • Project Code: 218815
  • Funding stream: FP7 | SP1 | SPA
,
EC| SMARTHG
Project
SMARTHG
Energy Demand Aware Open Services for Smart Grid Intelligent Automation
  • Funder: European Commission (EC)
  • Project Code: 317761
  • Funding stream: FP7 | SP1 | ICT
27 references, page 1 of 2

[1] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3-34, 1995. [OpenAIRE]

[2] R. Alur, T.A. Henzinger, G. Lafferriere, and G.J. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88(7):971-984, 2000. [OpenAIRE]

[3] Rajeev Alur, Thao Dang, and Franjo Ivancˇic´. Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. on Embedded Computing Sys., 5(1):152-199, 2006.

[4] Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng., 22(3):181-201, 1996.

[5] Paul C. Attie, Anish Arora, and E. Allen Emerson. Synthesis of fault-tolerant concurrent programs. ACM Trans. on Program. Lang. Syst., 26(1):125-185, 2004.

[6] A. Bemporad. Hybrid Toolbox - User's http://www.ing.unitn.it/ bemporad/hybrid/toolbox.

[10] CUDD Web Page: http://vlsi.colorado.edu/ fabio/, 2004.

[11] G. Della Penna, D. Magazzeni, A. Tofani, B. Intrigila, I. Melatti, and E. Tronci. Automated Generation of Optimal Controllers through Model Checking Techniques, volume 15 of LNEE. Springer, 2008.

[12] Goran Frehse. Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transf., 10(3):263-279, 2008.

[13] Minyue Fu and Lihua Xie. The sector bound approach to quantized feedback control. IEEE Trans. on Automatic Control, 50(11):1698-1711, 2005. [OpenAIRE]

[14] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. STTT, 1(1):110-122, 1997.

[15] Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata? J. of Computer and System Sciences, 57(1):94-124, 1998.

[16] Thomas A. Henzinger and Joseph Sifakis. The embedded systems design challenge. In FM, LNCS 4085, pages 1-15, 2006.

[17] Susmit Jha, Sanjit A. Seshia, and Ashish Tiwari. Synthesis of optimal switching logic for hybrid systems. In EMSOFT, pages 107-116. ACM, 2011. [OpenAIRE]

[18] W. Kim, M. S. Gupta, G.-Y. Wei, and D. M. Brooks. Enabling on-chip switching regulators for multi-core processors using current staggering. In ASGI, 2007.

27 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Preprint . Conference object . 2012

On Model Based Synthesis of Embedded Control Software

Vadim Alimguzhin; Federico Mari; Igor Melatti; Ivano Salvo; Enrico Tronci;