×

Specification and analysis of timing requirements for real-time systems in the CBD approach. (English) Zbl 1118.68094

Summary: 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.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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
[2] Bernardi S, Donatelli S, Merseguer J (2002) From UML sequence diagrams and statecharts to analyzable Petri net models. In: Proceedings of WOSP 2002
[3] Eclipse (2006) Eclipse modeling project. http://www.eclipse.org/modeling/
[4] Ghezzi, C.; Mandrioli, D.; Morasca, S.; Pezze, M., A unified high-level Petri net formalism for time-critical systems, IEEE Trans Softw Eng, 17, 2, 160-172 (1991) · doi:10.1109/32.67597
[5] Graf, S.; Ober; Ober, I., Timed annotations with UML, Proceedings of specification and validation of UML models for real time and embedded systems (2003), San Francisco: FortMason Center, San Francisco
[6] Harel, D., Statecharts: a visual formalism for complex systems, Sci Comput Program, 8, 3, 231-274 (1987) · Zbl 0637.68010 · doi:10.1016/0167-6423(87)90035-9
[7] Jacobson, I.; Christerson, M.; Jonson, P.; Overgarrd, G., Object-oriented software engineering: a use case driven approach (1992), Reading: Addison-Wesley, Reading · Zbl 0803.68020
[8] 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
[9] 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
[10] 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
[11] Kopetz, H.; Finkelstein, A., Software engineering for real-time: a roadmap, Proceedings of the future of software engineering (2000), New York: ACM, New York
[12] 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
[13] McUmber WE, Cheng BHC (2001) A general framework for formalizing UML with formal language. In: Proceedings of the 23rd international conference on software engineering
[14] Merlin PM, Farber DJ (1976) Recoverability of communication protocols implications of a theoretical study. IEEE Trans Commun pp 1036-1043 · Zbl 0362.68096
[15] Milner, R., Communication and concurrency (1989), New York: Prentice Hall, New York · Zbl 0683.68008
[16] Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4)
[17] Ommering, RV; Linden, FVD; Kramer, J.; Magee, J., The koala component model for consumer electronics software, IEEE Comput, 33, 3, 78-85 (2000)
[18] Peng, D.; Shin, KG, Modeling of concurrent task execution in a distributed system for real-time control, IEEE Trans Comput C, 36, 4, 500-516 (1987)
[19] Ramchandani C (1974) Analysis of asynchronous concurrent systems by Petri nets. MA:MIT TR-120 (Project MAC), MIT
[20] 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
[21] Schmidt, DC; Kuhns, F., An overview of the real-time CORBA specification, Computer, 33, 6, 56-65 (2000) · doi:10.1109/2.846319
[22] Schmidt DC, et al. (2006) Real-time cORBA with TAO. http://www.cs.wustl.edu/ schmidt/TAO.html
[23] Selic, B.; Motus, L., Using models in real-time software design, IEEE Control Syst, 23, 3, 31-42 (2003) · doi:10.1109/MCS.2003.1200244
[24] 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
[25] 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)
[26] Wang, N., Total quality of service provisioning in middleware and applications, The Journal of microprocessors and microsystems, 27, 2, 45-54 (2003) · doi:10.1016/S0141-9331(02)00096-0
[27] Wirth N (1977) Toward a discipline of real-time programming. Commun ACM 20(8) · Zbl 0362.68043
[28] Yeh WJ (1993) Controlling state explosion in reachability. PhD thesis, Purdue University
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.