
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Giacomo Bucci, Luigi Sassoli, Enrico Vicario, "Correctness Verification and Performance Analysis of RealTime Systems Using Stochastic Preemptive Time Petri Nets," IEEE Transactions on Software Engineering, vol. 31, no. 11, pp. 913927, November, 2005.  
BibTex  x  
@article{ 10.1109/TSE.2005.122, author = {Giacomo Bucci and Luigi Sassoli and Enrico Vicario}, title = {Correctness Verification and Performance Analysis of RealTime Systems Using Stochastic Preemptive Time Petri Nets}, journal ={IEEE Transactions on Software Engineering}, volume = {31}, number = {11}, issn = {00985589}, year = {2005}, pages = {913927}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2005.122}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Correctness Verification and Performance Analysis of RealTime Systems Using Stochastic Preemptive Time Petri Nets IS  11 SN  00985589 SP913 EP927 EPD  913927 A1  Giacomo Bucci, A1  Luigi Sassoli, A1  Enrico Vicario, PY  2005 KW  Index Terms Realtime reactive systems KW  preemptive scheduling KW  correctness verification KW  performance and dependability evaluation KW  discrete time KW  maximal step semantics KW  confusion KW  well definedness KW  stochastic preemptive Time Petri nets. VL  31 JA  IEEE Transactions on Software Engineering ER   
[1] R.K. Ahuja, T.L. Magnanti, and J.B. Orlin, Network Flows. Prentice Hall, 1993.
[2] R. Alur and D.L. Dill, “Automata for Modeling RealTime Systems,” Proc. 17th Int'l Colloquium on Automata, Languages, and Programming, 1990.
[3] R. Alur and T.A. Henzinger, “Logics and Models of RealTime: A Survey,” RealTime: Theory in Practice, 1992.
[4] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi, “Times— A Tool for Modelling and Implementation of Embedded Systems,” Proc. Eighth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2002.
[5] H. BenAbdallah, J.Y. Choi, D. Clarke, Y.S. Kim, I. Lee, and H.L. Xie, “A Process Algebraic Approach to the schedulability Analysis of RealTime Systems,” RealTime Systems, vol. 15, no. 3, pp. 189219, 1998.
[6] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “UPPAAL: A ToolSuite for Automatic Verification of RealTime Systems,” Hybrid Systems III, 1996.
[7] A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. Le Guernic, and R. DeSimone, “The Synchronous Languages 12 Years Later,” Proc. IEEE, vol. 91, no. 1, pp. 6483, Jan. 2003.
[8] G. Berry and G. Gonthier, “The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation,” Science of Computer Programming, vol. 19, no. 2, pp. 87152, 1992.
[9] B. Berthomieu and M. Diaz, “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 17, no. 3, Mar. 1991.
[10] B. Berthomieu and M. Menasche, “An Enumerative Approach for Analyzing Time Petri Nets,” Proc. IFIP Congress, Sept. 1983.
[11] B. Berthomieu, P.O. Ribet, and F. Vernadat, “The Tool TINAConstruction of Abstract State Spaces for Petri Nets and Time Petri Nets,” Int'l J. Production Research, 2004.
[12] A. Bobbio and A. Horvath, “Petri Nets with Discrete Phase Type Timing: A Bridge between Stochastic and Functional Analysis,” Electronic Notes in Theoretical Computer Science, vol. 52, no. 3, 2001.
[13] A. Bobbio, A. Puliafito, M. Scarpa, and M. Telek, “WebSPN: NonMarkovian Stochastic Petri Net Tool,” Proc. 18th Int'l Conf. Application and Theory of Petri Nets, June 1997.
[14] A. Bobbio, A. Puliafito, M. Telek, and K. Trivedi, “Recent Developments in NonMarkovian Stochastic Petri Nets,” J. Systems Circuits and Computers, vol. 8, no. 1, pp. 119158, 1998.
[15] A. Bobbio and M. Scarpa, “Kronecker Representation of Stochastic Petri Nets with Discrete PH Distributions,” Proc. Third IEEE Ann. Int'l Computer Performance and Dependability Symp. (IPDS '98), Sept. 1998.
[16] R. Bruni, J. Meseguer, U. Montanari, and V. Sassone, “A Comparison of Petri Net Semantics under the Collective Token Philosophy,” Proc. Asian Computing Science Conf. (ASIAN), pp. 225244, 1998.
[17] G. Bucci and E. Vicario, “Compositional Validation of TimeCritical Systems Using Communicating Time Petri Nets,” IEEE Trans. Software Eng., vol. 21, no. 12, Dec. 1995.
[18] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, “Modeling Flexible RealTime Systems with Preemptive Time Petri Nets,” Proc. 15th Euromicro Conf. RealTime Systems (ECRTS03), July 2003.
[19] G. Bucci, L. Sassoli, and E. Vicario, “A Discrete Time Model for Performance Evaluation and Correctness Verification of RealTime Systems,” Proc. 10th Int'l Workshop Petri Nets and Performance Models (PNPM '03), Sept. 2003.
[20] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, “Timed State Space Analysis of RealTime Preemptive Systems,” IEEE Trans. Software Eng., vol. 30, no. 2, pp. 97111, Feb. 2004.
[21] G. Bucci, L. Sassoli, and E. Vicario, “Oris: A Tool for State Space Analysis of RealTime Preemptive Systems,” Proc. First Int'l Conf. the Quantitative Evaluation of Systems (QEST '04), Sept. 2004.
[22] G. Bucci, R. Piovosi, L. Sassoli, and E. Vicario, “Introducing Probability within State Class Analysis of DenseTimeDependent Systems,” Proc. Int'l Conf. the Quantitative Evaluation of Systems (QEST '05), Sept. 2005.
[23] P. Buchholz and I.V. Tarasyuk, “Net and Algebraic Approaches to Probabilistic Modeling,” Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science, pp. 3164, 2001.
[24] G. Buttazzo, Hard RealTime Computing Systems. Norwell, Mass.: Kluwer, 1997.
[25] M. Caccamo, L. Abeni, G.C. Buttazzo, and G. Lipari, “Elastic Scheduling for Flexible Workload Management,” IEEE Trans. Computers, 2002.
[26] F. Cassez and K.G. Larsen, “The Impressive Power of Stopwatches,” Proc. 11th Int'l Conf. Concurrency Theory, pp. 138152, Aug. 2000.
[27] A. Cervin, “Improved Scheduling of Control Tasks,” Proc. 11th Euromicro Conf. RealTime Systems, pp. 410, June 1999.
[28] A. Cervin, “Merging RealTime and Control Theory for Improving the Performance of Embedded Control Systems,” research report, Sept. 2004.
[29] A. Cervin, B. Lincoln, J. Eker, K.E. Ârzén, and G. Buttazzo, “The Jitter Margin and Its Application in the Design of RealTime Control Systems,” Proc. 10th Int'l Conf. RealTime and Embedded Computing Systems and Applications (RTCSA), Aug. 2004.
[30] G. Chiola, M. AjmoneMarsan, G. Balbo, and G. Conte, “Generalized Stochastic Petri Nets: A Definition at the Net Level and Its Implications,” IEEE Trans. Software Eng., Feb. 1993.
[31] G. Ciardo, “Discrete Time Markovian Stochastic Petri Nets,” Proc. Second Workshop Numerical Solution of Markovian Chains, 1995.
[32] G. Ciardo and R. Zijal, “Well Defined Sthocastic Petri Nets” Proc. Fourth Int'l Workshop Modeling Analysis and Simulation of Computer and Telecomunication Systems (MASCOTS '96), 1996.
[33] G. Ciardo, R. Zijal, and G. Hommel, “Discrete Deterministic and Stochastic Petri Nets” Measurement, Modeling, and Valuation of Computer and CommunicationSystems, pp. 103117, Sept. 1997.
[34] E.M. Clarke, E.A. Emerson, and A. Sistla, “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications,” ACM Trans. Programming Language, vol. 8, no. 2, pp. 244263, 1986.
[35] C. Courcoubetis and S. Tripakis, “Probabilistic Model Checking: Formalisms and Algorithms for Discrete and RealTime Systems,” Verification of Digital and Hybrid Systems, pp. 183219, 2000.
[36] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, 1996.
[37] R. De Nicola and F.W. Van Draager, “Action versus State Based Logics for Transition Systems,” Proc. LITP Spring School on Theoretical Computer Science, pp. 407419, 1990.
[38] E. Fersman, P. Pettersson, and W. Yi, “Timed Automata with Asynchronous Processes: Schedulability and Decidability,” Tools and Algorithms for Construction and Analysis of Systems, 2002.
[39] K. GosevaPopstojanova and K.S. Trivedi, “Stochastic Modeling Formalisms for Dependability, Performance and Performability,” Performance Evaluation— Origins and Directions, pp. 385404, 2000.
[40] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” Logics and Models of Concurrent Systems (NATO), 1985.
[41] A. Horvath, A. Puliafito, M. Scarpa, and M. Telek, “Analysis and Evaluation of NonMarkovian Stochastic Petri Nets,” Proc. 11th Int'l Conf. Computer Performance Evaluation (TOOLS), pp. 171187, 2000.
[42] K. Jay, L. Kevin, and B. Kenny, “Building Flexible RealTime System Using the Flex Language,” Computer, 1991.
[43] I. Lee, P. BremondGregoire, and R. Gerber, “A Process Algebraic Approach to the Specification and Analysis of Resource Bound RealTime Systems,” Proc. IEEE, vol. 82, no. 1, pp. 158171, Jan. 1994.
[44] I. Lee, J.Y. Choi, H.H. Kwak, A. Philippou, and O. Sokolsky, “A Family of ResourceBound RealTime Process Algebras,” Proc. 21st Int'l Conf. Formal Techniques for Networked and Distributed Systems (FORTE '01), Aug. 2001.
[45] M. Ajmone Marsan, G. Balbo, and G. Conte, “A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems,” ACM Trans. Computer Systems, vol. 2, no. 2, pp. 93122, May 1984.
[46] J. McManis and P. Varaiya, “Suspension Automata: A Decidable Class of Hybrid Automata,” Proc. Computer Aided Verification: Sixth Int'l Conf. (CAV '94), June 1994.
[47] P. Merlin and D.J. Farber, “Recoverability of Communication Protocols,” IEEE Trans. Comm., vol. 24, no. 9 Sept. 1976.
[48] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling RealTime Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, Sept. 1992.
[49] D. Lime and O.H. Roux, “Expressiveness and Analysis of Scheduling Extended Time Petri Nets,” Proc. Fifth IFAC Conf. Fieldbus and Their Applications (FET 2003), July 2003.
[50] O. Sokolsky, I. Lee, and H. BenAbdallah, “Specification and Analysis of RealTime Systems with PARAGON,” Annals of Software Eng., vol. 7 1999.
[51] E. Smith, “On the Border of Causality: Contact and Confusion,” Theoretical Computer Science, vol. 153, pp. 275270, 1996.
[52] J.A. Stankovic and K. Ramamritham, “What Is Predictability for RealTime Systems,” J. Realtime Systems, vol. 2 Dec. 1990.
[53] A.S. Tanenbaum, Modern Operating Systems. Prentice Hall, 2001.
[54] E. Teruel, G. Franceschinis, and M. DePierro, “Well Defined Generalized Stochastic Petri Nets: A Net Level Method to Specify Priorities,” IEEE Trans. Software Eng., vol. 29, Nov. 2003.
[55] M.Y. Vardi, “Automatic Verification of Probabilistic Concurrent FiniteState Programs,” Proc. Symp. Foundations of Computer Science (FOCS '85), pp. 327338, 1985.
[56] E. Vicario, “Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., Aug. 2001.
[57] B. Wittenmark and N. Trngren, “Timing Problems in RealTime Control Systems,” Proc. Am. Control Conf., 1995.
[58] R. Zijal, “Discrete Time Deterministic and Stochastic Petri Nets,” Proc. Int'l Workshop Quality of Comm.Based Systems, pp. 123136, 1994.
[59] A. Zimmermann, J. Freiheit, and G. Hommel, “Discrete Time Stochastic Petri Nets for Modeling and Evaluation of RealTime Systems,” Proc. Int'l Parallel and Distributed Processing Symp., 2001.