Formal Design and Verification of Real-Time Embedded Software

  • Pao-Ann Hsiung
  • Shang-Wei Lin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3302)


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.


application framework code generation real-time embedded software formal synthesis formal verification scheduling software components UML modeling 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.: Automata for modeling real-time systems. Theoretical Computer Science 126(2), 183–236 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  5. 5.
    Douglass, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison Wesley Longman, Inc., Reading (1999)Google Scholar
  6. 6.
    Fayad, M., Schmidt, D.: Object-oriented application frameworks. Communications of the ACM, Special Issue on Object-Oriented Application Frameworks 40 (October 1997)Google Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Hsiung, P.-A.: Embedded software verification in hardware-software codesign. Journal of Systems Architecture - the Euromicro Journal 46(15), 1435–1450 (2000)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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),
  17. 17.
    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)Google Scholar
  18. 18.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    Rumbaugh, J., Booch, G., Jacobson, I.: The UML Reference Guide. Addison Wesley Longman, Redwood City (1999)Google Scholar
  22. 22.
    Samek, M.: Practical Statecharts in C/C++ Quantum Programming for Embedded Systems, CMP Books (2002)Google Scholar
  23. 23.
    Schmidt, D.: Applying design patterns and frameworks to develop object-oriented communication software. In: Handbook of Programming Languages, vol. I (1997)Google Scholar
  24. 24.
    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)Google Scholar
  25. 25.
    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)Google Scholar
  26. 26.
    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)Google Scholar
  27. 27.
    Selic, B., Gullekan, G., Ward, P.T.: Real-time Object Oriented Modeling. John Wiley and Sons, Inc., Chichester (1994)zbMATHGoogle Scholar
  28. 28.
    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)CrossRefGoogle Scholar
  29. 29.
    Wang, F., Hsiung, P.-A.: Efficient and user-friendly verification. IEEE Transactions on Computers 51(1), 61–83 (2002)MathSciNetCrossRefGoogle Scholar
  30. 30.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Pao-Ann Hsiung
    • 1
  • Shang-Wei Lin
    • 1
  1. 1.Department of Computer Science and Information EngineeringNational Chung-Cheng UniversityChiayiTaiwan, ROC

Personalised recommendations