Specification and analysis of timing requirements for real-time systems in the CBD approach
Tóm tắt
In real-time software, not only computation errors but also timing errors can cause system failures, which eventually result in significant physical damages or threats to human life. To efficiently guarantee the timely execution of expected functions, it is necessary to clearly specify and formally verify timing requirements before performing detailed system design. With the expected benefit of reusability and extensibility, component technology has been gradually applied to developing industrial applications including real-time systems. However, most of component-based approaches applied to real-time systems lack in a systematic and rigorous approach to specifying and verifying timing requirements at an earlier development stage.
This paper proposes a component-based approach to specifying and verifying timing requirements for real-time systems in a systematic and compositional manner. We first describe behaviors of the constituent components including timing requirements in UML diagrams, and then translate the UML diagrams into MTER nets, an extension of TER nets, to perform timing analysis in a compositional way. The merit of the proposed approach is that the specification and analysis results can be reused and independently maintained.
Tài liệu tham khảo
Andrade SS, Macêdo R (2005) A component-based real-time architecture for distributed supervision and control applications. In: Proceedings of the 10th IEEE conference on emerging technologies and factory automation, pp 15–22
Bernardi S, Donatelli S, Merseguer J (2002) From UML sequence diagrams and statecharts to analyzable Petri net models. In: Proceedings of WOSP 2002
Eclipse (2006) Eclipse modeling project. http://www.eclipse.org/modeling/
Ghezzi C, Mandrioli D, Morasca S, Pezze M (1991) A unified high-level Petri net formalism for time-critical systems. IEEE Trans Softw Eng 17(2):160–172
Graf S, Ober, Ober I (2003) Timed annotations with UML. In: Proceedings of specification and validation of UML models for real time and embedded systems, FortMason Center, San Francisco
Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231–274
Jacobson I, Christerson M, Jonson P, Overgarrd G (1992) Object-oriented software engineering: a use case driven approach. Addison–Wesley, Reading
Jeng MD, Lu W (2002) Extension of UML and its conversion to Petri nets for semiconductor manufacturing modeling. In: Proceedings of the IEEE international conference on robotics & automation
Knapp A, Merz S, Rauh C (2002) Model checking timed UML state machines and collaborations. In: 7th international symposium formal techniques in real-time and fault tolerant systems (LNCS #2469), Oldenburg, Germany, pp 395–414
Konrad S, Campbell LA, Cheng BHC (2004) Automated analysis of timing information in UML diagram. In: Proceedings of the 19th international conference on automated software engineering
Kopetz H (2000) Software engineering for real-time: a roadmap. In: Finkelstein A (ed) Proceedings of the future of software engineering. ACM, New York
Lin CP, Lin YP, Jeng MD (2004) Design of intelligent manufacturing systems by using UML and Petri net. In: Proceedings of the international conference on networking, sensing & control
McUmber WE, Cheng BHC (2001) A general framework for formalizing UML with formal language. In: Proceedings of the 23rd international conference on software engineering
Merlin PM, Farber DJ (1976) Recoverability of communication protocols implications of a theoretical study. IEEE Trans Commun pp 1036–1043
Milner R (1989) Communication and concurrency, Prentice Hall, New York
Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4)
Ommering RV, Linden FVD, Kramer J, Magee J (2000) The koala component model for consumer electronics software. IEEE Comput 33(3):78–85
Peng D, Shin KG (1987) Modeling of concurrent task execution in a distributed system for real-time control. IEEE Trans Comput C 36(4):500–516
Ramchandani C (1974) Analysis of asynchronous concurrent systems by Petri nets. MA:MIT TR-120 (Project MAC), MIT
Sandström K, Fredriksson J, Åkerholm M (2004) Introducing a component technology for safety critical embedded real-time systems. In: Proceedings of the international conference on component-based software engineering, pp 194–208
Schmidt DC, Kuhns F (2000) An overview of the real-time CORBA specification. Computer 33(6):56–65
Schmidt DC, et al. (2006) Real-time cORBA with TAO. http://www.cs.wustl.edu/~schmidt/TAO.html
Selic B, Motus L (2003) Using models in real-time software design. IEEE Control Syst 23(3):31–42
Trowitzsch J, Zimmermann A, Hommel G (2005) Towards quantitative analysis of real-time UML using stochastic Petri nets. In: Proceedings of the 19th IEEE international parallel and distributed processing symposium, pp 139–145
Tsai JJP, Yang SJ, Chang YH (1995) Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications. IEEE Trans Softw Eng 21(1)
Wang N et al. (2003) Total quality of service provisioning in middleware and applications. The Journal of microprocessors and microsystems 27(2):45–54
Wirth N (1977) Toward a discipline of real-time programming. Commun ACM 20(8)
Yeh WJ (1993) Controlling state explosion in reachability. PhD thesis, Purdue University