This Article 
 Bibliographic References 
 Add to: 
VERTAF: An Application Framework for the Design and Verification of Embedded Real-Time Software
October 2004 (vol. 30 no. 10)
pp. 656-674
The growing complexity of embedded real-time software requirements calls for the design of reusable software components, the synthesis and generation of software code, and the automatic guarantee of nonfunctional properties such as performance, time constraints, reliability, and security. Available application frameworks targeted at the automatic design of embedded real-time software are poor in integrating functional and nonfunctional requirements. To bridge this gap, we reveal the design flow and the internal architecture of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates software component-based reuse, formal synthesis, and formal verification. A formal UML-based embedded real-time object model is proposed for component reuse. Formal synthesis employs quasi-static and quasi-dynamic scheduling with automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from SGM, by adapting it for embedded software. The proposed architecture for VERTAF is component-based and allows plug-and-play for the scheduler and the verifier. Using VERTAF to develop application examples significantly reduced design effort and illustrated how high-level reuse of software components combined with automatic synthesis and verification can increase design productivity.

[1] B. Achauer, “Objects in Real-Time Systems: Issues for Language Implementers,” ACM OOPS Messenger, vol. 7, pp. 21-27, Jan. 1996.
[2] R. Alur and D. Dill, “Automata for Modeling Real-Time Systems,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-236, Apr. 1994.
[3] T. Amnell, E. Fersman, L. Mokrushin, P. Petterson, and W. Yi, “TIMES: A Tool for Schedulability Analysis and Code Generation of Real-Time Systems,” Proc. First Int'l Workshop Formal Modeling and Analysis of Timed Systems (FORMATS), Sept. 2003.
[4] B-toolkit, B-core (UK) Ltd., http:/, 2002
[5] J.A. Bannister and K.S. Trivedi, “Task Allocation in Fault-Tolerant Distributed Systems,” Acta Informatica, vol. 20, no. 3, pp. 261-281, 1983.
[6] S. Bernardi, S. Donatelli, and J. Merseguer, “From UML Sequence Diagrams and Statecharts to Analyzable Petri Net Models,” Proc. Third Int'l Workshop Software and Performance (WOSP '02), pp. 35-45, July 2002.
[7] G. Bollella, J. Gosling, B. Brosgol, P. Dibble, S. Furr, and M. Turnbull, The Real-Time Specification for Java. Addison Wesley, Jan. 2000.
[8] J. Browne, “Object-Oriented Development of Real-Time Systems: Verification of Functionality and Performance,” ACM OOPS Messenger, special issue on object-oriented real-time systems, vol. 7, pp. 59-62, Jan. 1996.
[9] Y. Choi, S. Rayadurgam, and M.P.E. Heimdahl, “Automatic Abstraction for Model Checking Software Systems with Interrelated Numeric Constraints,” Proc. Eighth European Software Eng. Conf. and Ninth ACM SIGSOFT Symp. Foundation of Software Eng., Sept. 2001.
[10] E.M. Clarke and E.A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” Proc. Logics of Programs Workshop, 1981.
[11] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999.
[12] H. Dammag and N. Nissanke, “Safecharts for Specifying and Designing Safety Critical Systems,” Proc. 18th IEEE Symp. Reliable Distributed Systems, Oct. 1999.
[13] DO-178B: Software Considerations in Airborne Systems and Equipment Certification, RTCA, 1992.
[14] B.P. Douglass, Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison Wesley, Nov. 1999.
[15] M. Elkoutbi and R.K. Keller, “Modeling Interactive Systems with Hierarchical Colored Petri Nets,” Proc. Advanced Simulation Technologies Conf., pp. 432-437, Apr. 1998.
[16] Esterel Technologies, http:/, 2003.
[17] M. Fayad and D. Schmidt, “Object-Oriented Application Frameworks,” Comm. ACM, special issue on object-oriented application frameworks, vol. 40, Oct. 1997.
[18] O. Fengler, W. Fengler, and T. Hummel, “Verification Method for Modeling Cooperating Processes with Colored Sequence Diagrams,” Proc. 23rd IASTED Int'l Conf. Modelling, Identification, and Control (MIC '04), Feb. 2004.
[19] M. Gergeleit, J. Kaiser, and H. Streich, “Checking Timing Constraints in Distributed Object-Oriented Programs,” ACM OOPS Messenger, special issue on object-oriented real-time systems, vol. 7, pp. 51-58, Jan. 1996.
[20] A. Grimshaw, A. Silberman, and J. Liu, “Real-Time Mentat, A Data-Driven Object-Oriented System,” Proc. IEEE Globecom Conf., pp. 141-147, Nov. 1989.
[21] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, “The Synchronous Dataflow Programming Language Lustre,” Proc. IEEE, vol. 79, no. 9, pp. 1305-1320, 1991.
[22] D. Hammer, L. Welch, and O. vanRoosmalen, “A Taxonomy for Distributed Object-Oriented Real-Time Systems,” ACM OOPS Messenger, special issue on object-oriented real-time systems, vol. 7, pp. 78-85, Jan. 1996.
[23] H.A. Hansson, H.W. Lawson, M. Stromberg, and S. Larsson, “BASEMENT: A Distributed Real-Time Architecture for Vehicle Applications,” Real-Time Systems, vol. 11, no. 3, pp. 223-244, 1996.
[24] C.L. Heitmeyer, J. Kirby, B. Labaw, and R. Bharadwaj, “SCR*: A Toolset for Specifying and Analyzing Software Requirements,” Proc. 10th Int'l Conf. Computer-Aided Verification, pp. 526-531, 1998.
[25] T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for Real-Time Systems,” Proc. IEEE Logics in Computer Science, 1992.
[26] T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “Decomposing Refinement Proofs Using Assume-Guarantee Reasoning,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD '00), pp. 245-252, 2000.
[27] P.-A. Hsiung, “RTFrame: An Object-Oriented Application Framework for Real-Time Applications,” Proc. 27th Int'l Conf. Technology of Object-Oriented Languages and Systems (TOOLS '98), pp. 138-147, Sept. 1998.
[28] P.-A. Hsiung, “Embedded Software Verification in Hardware-Software Codesign,” J. Systems Architecture-the Euromicro J., vol. 46, no. 15, pp. 1435-1450, Nov. 2000.
[29] P.-A. Hsiung and S.-Y. Cheng, “Automating Formal Modular Verification of Asynchronous Real-Time Embedded Systems,” Proc. 16th Int'l Conf. VLSI Design, (VLSI '03), pp. 249-254, Jan. 2003.
[30] P.-A. Hsiung and C.-Y. Lin, “Synthesis of Real-Time Embedded Software with Local and Global Deadlines,” Proc. First ACM/IEEE/IFIP Int'l Conf. Hardware-Software Codesign and System Synthesis (CODES+ISSS '03), pp. 114-119, Oct. 2003.
[31] P.-A. Hsiung, C.-Y. Lin, and T.-Y. Lee, “Quasi-Dynamic Scheduling for the Synthesis of Real-Time Embedded Software with Local and Global Deadlines,” Proc. Ninth Int'l Conf. Real-Time and Embedded Computing Systems and Applications (RTCSA '03), Feb. 2003.
[32] Y. Ishikawa, H. Tokuda, and C.W. Mercer, “Object-Oriented Real-Time Language Design: Constructs for Timing Constraints,” ACM SIGPLAN Notices, Proc. ECOOP/OOPSLA '90 Confs., vol. 25, pp. 289-298, Oct. 1990.
[33] K.H. Kim, “APIs for Real-Time Distributed Object Programming,” Computer, vol. 33, no. 6, pp. 72-80, June 2000.
[34] A. Knapp, S. Merz, and C. Rauh, “Model Checking Timed UML State Machines and Collaboration,” Proc. Seventh Int'l Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, Sept. 2002.
[35] T. Kuan, W.-B. See, and S.-J. Chen, “An Object-Oriented Real-Time Framework and Development Environment,” Proc. OOPSLA '95 Conf. Workshop 18, 1995.
[36] S. Kodase, S. Wang, and K.G. Shin, “Transforming Structural Model to Runtime Model of Embedded Software with Real-Time Constraints,” Proc. Design, Automation and Test in Europe Conf., pp. 170-175, Mar. 2003.
[37] L. Lavazza, “A Methodology for Formalizing Concepts Underlying the DESS Notation,” Software Development Process for Real-Time Embedded Software Systems, EUREKA-ITEA project D1.7.4, http:/, Dec. 2001.
[38] W.-S. Liao and P.-A. Hsiung, “FVP: A Formal Verification Platform for SoC,” Proc. 16th IEEE Int'l SoC Conf., Sept. 2003.
[39] C. Liu and J. Layland, “Scheduling Algorithms for Multiprogramming in a Hard-Real Time Environment,” J. ACM, vol. 20, pp. 46-61, Jan. 1973.
[40] D. de Niz and R. Rajkumar, “Time Weaver: A Software-Through-Models Framework for Embedded Real-Time Systems,” Proc. Int'l Workshop Languages, Compilers, and Tools for Embedded Systems, pp. 133-143, June 2003.
[41] M. Potkonjak and W. Wolf, “A Methodology and Algorithms for the Design of Hard Real-Time Multitasking ASICs,” ACM Trans. Design Automation of Electronic Systems, vol. 4, no. 4, pp. 430-459, Oct. 1999.
[42] J.-P. Queille and J. Sifakis, “Specification and Verification of Concurrent Systems in CESAR,” Proc. Int'l Symp. Programming, 1982.
[43] R. Ratner, E. Shapiro, H. Zeidler, S. Wahlstrom, C. Clark, and J. Goldberg, “Design of a Fault-Tolerant Airborne Digital Computer,” Computational Requirements and Technology, vol. 2, SRI Final Report, NASA Contract NAS1-10920, 1973.
[44] E.E. Roubtsova, J. van Katwijk, W.J. Toetenel, C. Pronk, and R.C.M. de Rooij, “Specification of Real-Time Systems in UML,” Electronic Notes in Theoretical Computer Science (ENTCS), vol. 39, no. 3, 2000.
[45] J. Rumbaugh, G. Booch, and I. Jacobson, The UML Reference Guide. Addison Wesley Longman, 1999.
[46] J.A. Saldhana and S.M. Shatz, “UML Diagrams to Object Petri Net Models: An Approach for Modeling and Analysis,” Proc. Int'l Conf. Software Eng. and Knowledge Eng. (SEKE), pp. 103-110, July 2000.
[47] M. Samek, Practical Statecharts in C/C++ Quantum Programming for Embedded Systems. CMP Books, 2002.
[48] D. Schmidt, “Applying Design Patterns and Frameworks to Develop Object-Oriented Communication Software,” Handbook of Programming Languages, vol. I 1997.
[49] W.-B. See and S.-J. Chen, “Object-Oriented Real-Time System Framework,” Domain-Specific Application Frameworks, M.E. Fayad and R.E. Johnson, eds., pp. 327-338, 2000.
[50] B. Selic, “Modeling Real-Time Distributed Software Systems,” Proc. Fourth Int'l Workshop Parallel and Distributed Real-Time Systems, pp. 11-18, 1996.
[51] B. Selic, “An Efficient Object-Oriented Variation of the Statecharts Formalism for Distributed Real-Time Systems,” Proc. IFIP Conf. Hardware Description Languages and Their Applications, 1993.
[52] B. Selic, G. Gullekan, and P.T. Ward, Real-Time Object Oriented Modeling. John Wiley and Sons, 1994.
[53] T.-Y. Shen, “Assume-Guarantee Based Formal Verification of Hierarchical Software Designs,” master's thesis, Dept. of Computer Software and Information Eng., Nat'l Chung Cheng Univ., July 2003.
[54] D.B. Stewart, R.A. Volpe, and P.K. Khosla, “Design of Dynamically Reconfigurable Real-Time Software Using Port-Based Objects,” IEEE Trans. Software Eng., vol. 23, no. 12, Dec. 1997.
[55] F.-S. Su and P.-A. Hsiung, “Extended Quasi-Static Scheduling for Formal Synthesis and Code Generation of Embedded Software,” Proc. 10th IEEE/ACM Int'l Symp. Hardware/Software Codesign (CODES '02), pp. 211-216, May 2002.
[56] C. Szyperski, Component Software: Beyond Object-Oriented Programming. Addison-Wesley, 2002.
[57] J.M. Thompson, M.P.E. Heimdahl, and S.P. Miller, “Specification-Based Prototyping for Embedded Systems,” Proc. Seventh ACM SIGSOFT Symp. Foundations of Software Eng., pp. 163-179, Sept. 1999.
[58] F. Wang and P.-A. Hsiung, “Efficient and User-Friendly Verification,” IEEE Trans. Computers, vol. 51, no. 1, pp. 61-83, Jan. 2002.
[59] S. Wang, S. Kodase, and K.G. Shin, “Automating Embedded Software Construction and Analysis with Design Models,” Proc. Int'l Conf. Euro-uRapid, Dec. 2002.
[60] L.R. Welch, “A Metrics-Driven Approach for Utilizing Concurrency in Object-Oriented Real-Time Systems,” ACM OOPS Messenger, vol. 7, pp. 70-77, Jan. 1996.
[61] M. Zulkernine and R.E. Seviora, “Assume-Guarantee Supervisor for Concurrent Systems,” Proc. 15th Int'l Parallel and Distributed Processing Symp., pp. 1552-1560, Apr. 2001.

Index Terms:
Application framework, code generation, embedded real-time software, formal synthesis, formal verification, scheduling, software components, UML modeling.
Pao-Ann Hsiung, Shang-Wei Lin, Chih-Hao Tseng, Trong-Yen Lee, Jih-Ming Fu, Win-Bin See, "VERTAF: An Application Framework for the Design and Verification of Embedded Real-Time Software," IEEE Transactions on Software Engineering, vol. 30, no. 10, pp. 656-674, Oct. 2004, doi:10.1109/TSE.2004.68
Usage of this product signifies your acceptance of the Terms of Use.