×

zbMATH — the first resource for mathematics

Verifying distributed real-time properties of embedded systems via graph transformations and model checking. (English) Zbl 1103.68630
Summary: Component middleware provides dependable and efficient platforms that support key functional, and Quality of Service (QoS) needs of Distributed Real-time Embedded (DRE) systems. Component middleware, however, also introduces challenges for DRE system developers, such as evaluating the predictability of DRE system behavior, and choosing the right design alternatives before committing to a specific platform or platform configuration. Model-based technologies help address these issues by enabling design-time analysis, and providing the means to automate the development, deployment, configuration, and integration of component-based DRE systems. To this end, this paper applies model checking techniques to DRE design models using model transformations to verify key QoS properties of component-based DRE systems developed using Real-time CORBA. We introduce a formal semantic domain for a general class of DRE systems that enables the verification of distributed non-preemptive real-time scheduling. Our results show that model-based techniques enable design-time analysis of timed properties and can be applied to effectively predict, simulate, and verify the event-driven behavior of component-based DRE systems.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68M99 Computer system organization
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdeddaïm Y, Maler O (2002) Preemptive job-shop scheduling using stopwatch automata. In TACAS ’02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, London, UK, pp 113–126 · Zbl 1043.68510
[2] Agrawal A, Karsai G, Ledeczi A (2003) An End-to-End Domain-Driven Development Framework. In Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
[3] Alur R, Courcoubetis C, Dill DL (1993) Model-checking in dense real-timeInformation and Computation 104(1):2–34 · Zbl 0783.68076 · doi:10.1006/inco.1993.1024
[4] Alur R, Dill DL (1994) A theory of timed automataTheoretical Computer Science 126(2):183–235 · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[5] Arulanthu AB, O’Ryan C, Schmidt DC, Kircher M, Parsons J (2000) The Design and Performance of a Scalable ORB architecture for CORBA asynchronous messaging. In Proceedings of the Middleware Conference. ACM/IFIP
[6] Balarin F, Watanabe Y, Hsieh H, Lavagno L, Passerone C, Sangiovanni-Vincentelli A (2003) Metropolis: An integrated electronic system design environmentComputer 36(4):45–52 · Zbl 05088251 · doi:10.1109/MC.2003.1193228
[7] Blazewicz J, Lenstra J, Kan AR (1983) Scheduling subject to resource constraints: Classification and complexity Discrete Applied Mathematics, pp 11–24 · Zbl 0516.68037
[8] Bozga M, Graf S, Ober I, Ober I, Sifakis J (2004) The IF toolset Formal Methods for the Design of Real-Time Systems, LNCS 3185, pp 237–267 · Zbl 1105.68352
[9] Braberman VA, Felder M (1999) Verification of Real-Time Designs: Combining Scheduling Theory with Automatic Formal Verification. In Software Engineering-ESEC/FSE 99, pp 494–510
[10] Bradley S, Henderson W, Kendall D (1999) Using Timed Automata for Response Time Analysis of Distributed Real-Time Systems. In 24th IFAC/IFIP Workshop on Real-Time Programming WRTP 99, pp 143–148
[11] Buschmann F, Meunier R, Rohnert H, Sommerlad P, Stal M (1996) Pattern-oriented software architecture–A system of patterns. Wiley & Sons, New York
[12] Buttazzo GC (2005) Rate monotonic vs. EDF: Judgment day. Real-Time Systems 29:5–26 · Zbl 1097.68530 · doi:10.1023/B:TIME.0000048932.30002.d9
[13] Cornea R, Dutt N, Gupta R, Krueger I, Nicolau A, Schmidt D, Shukla S (2003) FORGE: A Framework for Optimization of Distributed Embedded Systems Software. In Proceedings of the International Parallel and Distributed Processing Symposium
[14] Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool KRONOS. In Proceedings of the DIMACS/SYCON Workshop on Hybrid Systems III: Verification and Control. Springer-Verlag, New York, Inc., pp 208–219
[15] de Niz D, Rajkumar R (2003) Time weaver: A Software-Through-Models Framework for Real-Time Systems. In Proceedings of LCTES
[16] Deshpande M, Schmidt DC, O’Ryan C, Brunsch D (2002) Design and Performance of Asynchronous Method Handling for CORBA. In Proceedings of Distributed Objects and Applications (DOA) · Zbl 1018.68614
[17] Doerr BS, Sharp DC (1999) Freeing Product Line Architectures from Execution Dependencies. In Proceedings of the 11th Annual Software Technology Conference
[18] Edmund J, Clarke M, Grumberg O, Peled DA (1999) Model checking. MIT Press
[19] Ericsson C, Wall A, Yi W (1999) Timed automata as task models for event-driven systems. In Proceedings of RTSCA ’99
[20] Gerdsmeier T, Cardell-Oliver R (2001) Analysis of scheduling behaviour using generic timed automata 42 · Zbl 0971.68010
[21] Gill CD, Gossett JM, Corman D, Loyall JP, Schantz RE, Atighetchi M, Schmidt DC (2005) Integrated adaptive QoS management in middleware: An empirical case studyJournal of Real-Time Systems 24
[22] Gokhale A, Balasubramanian K, Balasubramanian J, Krishna AS, Edwards GT, Deng G, Turkay E, Parsons J, Schmidt DC (2005) Model driven middleware: A new paradigm for deploying and provisioning distributed real-time and embedded applications The Journal of Science of Computer Programming: Special Issue on Model Driven Architecture, (to appear) · Zbl 1173.68386
[23] Gu Z, Shin K (2005) Model-checking of component-based real-time embedded software based on corba event service. In IEEE International Symposium on Object-Oriented Real-Time Distributed Computing
[24] Gu Z, Wang S, Kodase S, Shin KG (2003) An End-to-End Tool Chain for Multi-View Modeling and Analysis of Avionics Mission Computing Software. In Proceedings of Real-Time Systems Symposium
[25] Harrison TH, Levine DL, Schmidt DC (1997) The design and performance of a real-time CORBA event service. In Proceedings of the 12th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM Press, pp 184–200
[26] Hartmann S, Kolisch R (2000) Experimental evaluation of state-of-the-art heuristics for the resource-constrained project scheduling problem European Journal of Operations Research, 394–407 · Zbl 0985.90036
[27] Hatcliff J, Deng X, Dwyer MB, Jung G, Ranganath VP (2003) Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems. In Proceedings of International Conference on Software Engineering
[28] Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In POPL ’02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM Press, New York, NY, USA, pp 58–70 · Zbl 1323.68374
[29] Henzinger TA, Horowitz B, Kirsch CM (2001) Giotto: A time-triggered language for embedded programming. Lecture Notes in Computer Science 2211:166+ · Zbl 1050.68525
[30] Holzmann GJ (2004) The SPIN model checker: Primer and reference manual. Addison Wesley, hOL g 03:1 1.Ex
[31] Klein MH, Ralya T, Pollak B, Obenza R (1993) A practitioners handbook for real-time analysis: Guide to rate monotonic analysis for real-time systems. Kluwer
[32] Kr/vcál P, Yi W (2004) Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. In Jensen K, Podelski A (eds), Proc. of TACAS’04, Barcelona, Spain, ser. Lecture Notes in Computer Science, Springer-Verlag, vol. 2988, pp 236–250 · Zbl 1126.68456
[33] Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshellInt. Journal on Software Tools for Technology Transfer 1(1–2):134–152 · Zbl 1060.68577 · doi:10.1007/s100090050010
[34] Ledeczi A, Bakay A, Maroti M, Volgyesi P, Nordstrom G, Sprinkle J (2001) Composing Domain-Specific Design EnvironmentsComputer 44–51
[35] Liu CL, Layland JW (1973)Scheduling algorithms for multiprogramming in a hard-real-time environmentJ ACM 20(1):46–61 · Zbl 0265.68013 · doi:10.1145/321738.321743
[36] McManis J, Varaiya P (1994) Suspension automata: A decidable class of hybrid automata. In CAV ’94: Proceedings of the 6th International conference on Computer Aided Verification. Springer-Verlag, London, UK, pp 105–117
[37] Madl G, Abdelwahed S (2005) Model-based Analysis of Distributed Real-time Embedded System Composition. In EMSOFT 2005
[38] Object Management Group (2002a) CORBA component model. [Online]. Available: http://www.omg.org · Zbl 1014.68760
[39] Object Management Group (2002b) Real-time CORBA SpecificationOMG document formal/02-08-02 ed.
[40] Pettersson P, Larsen KG (2000) Uppaal2kBulletin of the European Association for Theoretical Computer Science 70:40–44
[41] Roll W (2003)Towards model-based and CCM-based applications for real-time systems. In ISORC ’03: Proceedings of the Sixth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC’03). IEEE computer society, pp 75–82
[42] Rumbaugh J, Jacobson I, Booch G (1998) The unified modeling language reference manual
[43] Schmidt DC, Gokhale A, Harrison TH, Parulkar G (1997) A high-performance endsystem architecture for real-time CORBAIEEE Communications Magazine 14(2)
[44] Schmidt DC, Stal M, Rohnert H, Buschmann F (2000) Pattern-oriented software architecture: Patterns for concurrent and networked objects, vol. 2. Wiley & Sons, New York · Zbl 1001.68025
[45] Sharp DC, Roll WC (2003) Model-based integration of reusable component-based avionics systems. In Proceedings of the Workshop on Model-Driven Embedded Systems in RTAS 2003
[46] Stankovic JA, Zhu R, Poornalingham R, Lu C, Yu Z, Humphrey M, Ellis B (2003) VEST: An aspect-based composition Tool for Real-time Systems. In Proceedings of the IEEE Real-Time Applications Symposium
[47] Sztipanovits J, Karsai G (1997) Model-Integrated ComputingIEEE Computer 110–112
[48] Tindell K, Clark J (1994) Holistic Schedulability Analysis for Distributed Hard Real-Time Systems Microprocessing and Microprogramming–Euromicro Journal (Special Issue on Parallel Embedded Real-Time Systems) 40:117–134
[49] Wang N, Schmidt DC, Parameswaran K, Kircher M (2000) Applying reflective middleware techniques to optimize a QoS-enabled CORBA component model implementation. In 24th Computer Software and Applications Conference. IEEE, Taipei, Taiwan
[50] World Wide Web Consortium (2004a) Extensible Markup Language (XML) 1.0 3rd edn
[51] World Wide Web Consortium (2004b) XSL Transformations (XSLT) Version 1.0
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.