Abstract
Currently available application frameworks that target at the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements. In this work, we reveal the internal architecture and design flow of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates software component-based reuse, formal synthesis, and formal verification. Component reuse is based on a formal UML real-time embedded object model. Formal synthesis employs quasi-static and quasi-dynamic scheduling with multi-layer portable efficient code generation, which can output either RTOS-specific application code or automatically-generated real-time executive with application code. Formal verification integrates a model checker kernel from SGM, by adapting it for embedded software. Application examples developed using VERTAF demonstrate significantly reduced design efforts as compared to that without VERTAF, which shows how high-level reuse of software components with automatic synthesis and verification increase design productivity.
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
Alur, R., Dill, D.: Automata for modeling real-time systems. Theoretical Computer Science 126(2), 183–236 (1994)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Proceedings of the Logics of Programs Workshop. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Douglass, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns, November 1999. Addison Wesley Longman, Inc., Reading (1999)
Fayad, M., Schmidt, D.: Object-oriented application frameworks. Communications of the ACM, Special Issue on Object-Oriented Application Frameworks 40 (October 1997)
Hansson, H.A., Lawson, H.W., Stromberg, M., Larsson, S.: BASEMENT: A distributed real-time architecture for vehicle applications. Real-Time Systems 11(3), 223–244 (1996)
Hsiung, P.-A.: RTFrame: An object-oriented application framework for real-time applications. In: Proceedings of the 27th International Conference on Technology of Object-Oriented Languages and Systems (TOOLS 1998), September 1998, pp. 138–147. IEEE Computer Society Press, Los Alamitos (1998)
Hsiung, P.-A.: Embedded software verification in hardware-software codesign. Journal of Systems Architecture - the Euromicro Journal 46(15), 1435–1450 (2000)
Hsiung, P.-A., Cheng, S.-Y.: Automating formal modular verification of asynchronous real-time embedded systems. In: Proceedings of the 16th International Conference on VLSI Design, VLSI 2003, New Delhi, India, January 2003, pp. 249–254. IEEE CS Press, Los Alamitos (2003)
Hsiung, P.-A., Lin, C.-Y.: Synthesis of real-time embedded software with local and global deadlines. In: Proceedings of the 1st ACM/IEEE/IFIP International Conference on Hardware-Software Codesign and System Synthesis CODES+ISSS 2003, Newport Beach, CA, USA, October 2003, pp. 114–119. ACM Press, New York (2003)
Hsiung, P.-A., Lin, C.-Y., Lee, T.-Y.: Quasi-dynamic scheduling for the synthesis of real-time embedded software with local and global deadlines. In: Chen, J., Hong, S. (eds.) RTCSA 2003. LNCS, vol. 2968, pp. 229–243. Springer, Heidelberg (2004)
Liu, C., Layland, J.: Scheduling algorithms for multiprogramming in a hardreal time environment. Journal of the Association for Computing Machinery 20, 46–61 (1973)
de Niz, D., Rajkumar, R.: TimeWeaver: A software-through-models framework for embedded real-time systems. In: Proceedings of the International Workshop on Languages, Compilers, and Tools for Embedded Systems, San-Diego, California, USA, June 2003, pp. 133–143 (2003)
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Rumbaugh, J., Booch, G., Jacobson, I.: The UML Reference Guide. Addison Wesley Longman, Amsterdam (1999)
Samek, M.: Practical Statecharts in C/C++ Quantum Programming for Embedded Systems, CMP Books (2002)
Schmidt, D.: Applying design patterns and frameworks to develop object-oriented communication software. In: Handbook of Programming Languages, vol. I (1997)
Selic, B., Gullekan, G., Ward, P.T.: Real-time Object Oriented Modeling. John Wiley and Sons, Inc., Chichester (1994)
Su, F.-S., Hsiung, P.-A.: Extended quasi-static scheduling for formal synthesis and code generation of embedded software. In: Proceedings of the 10th IEEE/ACM International Symposium on Hardware/Software Codesign, CODES 2002, Colorado, USA, May 2002, pp. 211–216. ACM Press, New York (2002)
Wang, F., Hsiung, P.-A.: Efficient and user-friendly verification. IEEE Transactions on Computers 51(1), 61–83 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hsiung, PA., Lin, SW. (2004). Automatic Synthesis and Verification of Real-Time Embedded Software. In: Yang, L.T., Guo, M., Gao, G.R., Jha, N.K. (eds) Embedded and Ubiquitous Computing. EUC 2004. Lecture Notes in Computer Science, vol 3207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30121-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-30121-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22906-3
Online ISBN: 978-3-540-30121-9
eBook Packages: Springer Book Archive