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 three techniques namely 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. The proposed architecture for VERTAF is component-based which allows plug-and-play for the scheduler and the verifier. The architecture is also easily extensible because reusable hardware and software design components can be added. Application examples developed using VERTAF demonstrate significantly reduced relative design effort as compared to design without VERTAF, which also shows how high-level reuse of software components combined 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.
Similar content being viewed by others
References
Alur, R., Dill, D.: Automata for modeling real-time systems. Theoretical Computer Science 126(2), 183–236 (1994)
Amnell, T., Fersman, E., Mokrushin, L., Petterson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems, FORMATS, Marseille, France (September 2003)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
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. 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), 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, 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, 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)
Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaboration. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–414. Springer, Heidelberg (2002)
Kuan, T., See, W.-B., Chen, S.-J.: An object-oriented real-time framework and development environment. In: Proceedings OOPSLA 1995 Workshop, vol. 18 (1995)
Kodase, S., Wang, S., Shin, K.G.: Transforming structural model to runtime model of embedded software with real-time constraints. In: Proceedings of Design, Automation and Test in Europe Conference, Munich, Germany, March 2003, pp. 170–175 (2003)
Lavazza, L.: A methodology for formalizing concepts underlying the DESS notation, Software Development Process for Real-Time Embedded Software Systems, EUREKA-ITEA project, D 1.7.4 (December 2001), http://www.dess-itea.org
Liao, W.-S., Hsiung, P.-A.: FVP: A formal verification platform for SoC. In: Proceedings of the 16th IEEE International SoC Conference, Portland, Oregon, USA. IEEE CS Press, Portland (2003)
Liu, C., Layland, J.: Scheduling algorithms for multiprogramming in a hard-real time environment. Journal of the Association for Computing Machinery 20, 46–61 (1973)
de Niz, D., Rajkumar, R.: Time Weaver: 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, Redwood City (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)
See, W.-B., Chen, S.-J.: Object-oriented real-time system framework. In: Fayad, M.E., Johnson, R.E. (eds.) Domain-Specific Application Frameworks, ch. 16, pp. 327–338. John Wiley, Chichester (2000)
Selic, B.: Modeling real-time distributed software systems. In: Proceedings of the 4th International Workshop on Parallel and Distributed Real-Time Systems, pp. 11–18 (1996)
Selic, B.: An efficient object-oriented variation of the statecharts formalism for distributed real-time systems. In: Proceedings of the IFIP Conference on Hardware Description Languages and Their Applications (1993)
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, 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)
Wang, S., Kodase, S., Shin, K.G.: Automating embedded software construction and analysis with design models. In: Proceedings of International Conference of Euro-uRapid, Frankfurt, Germany (December 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). Formal Design and Verification of Real-Time Embedded Software. In: Chin, WN. (eds) Programming Languages and Systems. APLAS 2004. Lecture Notes in Computer Science, vol 3302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30477-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-30477-7_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23724-2
Online ISBN: 978-3-540-30477-7
eBook Packages: Springer Book Archive