
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Jan Rakow, Ralf Wimmer, Bernd Becker, "Compositional Dependability Evaluation for STATEMATE," IEEE Transactions on Software Engineering, vol. 35, no. 2, pp. 274292, March/April, 2009.  
BibTex  x  
@article{ 10.1109/TSE.2008.102, author = {Eckard Böde and Marc Herbstritt and Holger Hermanns and Sven Johr and Thomas Peikenkamp and Reza Pulungan and Jan Rakow and Ralf Wimmer and Bernd Becker}, title = {Compositional Dependability Evaluation for STATEMATE}, journal ={IEEE Transactions on Software Engineering}, volume = {35}, number = {2}, issn = {00985589}, year = {2009}, pages = {274292}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2008.102}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Compositional Dependability Evaluation for STATEMATE IS  2 SN  00985589 SP274 EP292 EPD  274292 A1  Eckard Böde, A1  Marc Herbstritt, A1  Holger Hermanns, A1  Sven Johr, A1  Thomas Peikenkamp, A1  Reza Pulungan, A1  Jan Rakow, A1  Ralf Wimmer, A1  Bernd Becker, PY  2009 KW  Realtime and embedded systems KW  Fault tolerance KW  Modeling techniques KW  Reliability KW  availability KW  and serviceability KW  Model checking KW  Reliability KW  Design notations and documentation KW  State diagrams VL  35 JA  IEEE Transactions on Software Engineering ER   
[1] J. Hillston, A Compositional Approach to Performance Modelling. Cambridge Univ. Press, 1996.
[2] D. Kartson, G. Balbo, S. Donatelli, G. Franceschinis, and G. Conte, Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Inc., 1994.
[3] A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, “PRISM: A Tool for Automatic Verification of Probabilistic Systems,” Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, vol. 3920, pp.441444, 2006.
[4] C. Baier, H. Hermanns, J.P. Katoen, and B.R. Haverkort, “Efficient Computation of TimeBounded Reachability Probabilities in Uniform ContinuousTime Markov Decision Processes,” Theoretical Computer Science, vol. 345, no. 1, pp.226, 2005.
[5] H. Hermanns, Interactive Markov Chains and the Quest for Quantified Quality. Springer, 2002.
[6] ARP4761, Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. Soc. of Automotive Engineers, Aerospace Recommended Practice, 1996.
[7] E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, R. Wimmer, and B. Becker, “Compositional Performability Evaluation for STATEMATE,” Proc. Third Int'l Conf. Quantitative Evaluation of Systems, pp.167178, 2006.
[8] H. Hermanns and S. Johr, “Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems,” Proc. 37th Ann. IEEE/IFIP Int'l Conf. Dependable Systems and Networks, pp.718728, 2007.
[9] R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp, and B. Becker, “Sigref—A Symbolic Bisimulation Tool Box,” Proc. Fourth Int'l Symp. Automated Technology for Verification and Analysis, pp.477492, 2006.
[10] H. Hermanns and S. Johr, “May We Reach It? or Must We? in What Time? with What Probability?” Proc. 14th GI/ITG Conf. Measurement, Modeling and Evaluation of Computer and Comm. Systems, pp.125140, 2008.
[11] R.J. van Glabbeek and W.P. Weijland, “Branching Time and Abstraction in Bisimulation Semantics,” J. ACM, vol. 43, no. 3, pp.555600, 1996.
[12] N. Wolovick and S. Johr, “A Characterization of Meaningful Schedulers for ContinuousTime Markov Decision Processes,” Proc. Fourth Int'l Conf. Formal Modeling and Analysis of Timed Systems, vol. 4202, pp.352367, 2006.
[13] S. Johr, “Model Checking Compositional Markov Systems,” PhD thesis, Saarland Univ., 2007.
[14] D. Harel and A. Naamad, “The STATEMATE Semantics of Statecharts,” ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp.293333, 1996.
[15] D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGrawHill, 1998.
[16] W. Damm, B. Josko, H. Hungar, and A. Pnueli, “A Compositional RealTime Semantics of STATEMATE Designs,” Revised Lectures Int'l Symp. Compositionality: The Significant Difference, pp.186238, 1998.
[17] J.P. Katoen, M. Khattri, and I.S. Zapreev, “A Markov Reward Model Checker,” Proc. Second Int'l Conf. Quantitative Evaluation of Systems, pp.243244, 2005.
[18] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[19] R.K. Brayton, G.D. Hachtel, A.L. SangiovanniVincentelli, F. Somenzi, A. Aziz, S.T. Cheng, S.A. Edwards, S.P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa, “VIS: A System for Verification and Synthesis,” Proc. Eighth Int'l Conf. Computer Aided Verification, 1996.
[20] R. Drechsler and B. Becker, Binary Decision Diagrams—Theory and Implementation. Kluwer Academic Publishers, 1998.
[21] S. Blom and S. Orzan, “Distributed Branching Bisimulation Reduction of State Spaces,” Electronic Notes in Theoretical Computer Science, vol. 89, no. 1, pp.99113, 2003.
[22] A. Bouali and R. de Simone, “Symbolic Bisimulation Minimization,” Proc. Fourth Int'l Work Computer Aided Verification, pp.96108, 1992.
[23] S. Derisavi, “A Symbolic Algorithm for Optimal Markov Chain Lumping,” Proc. 13th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.139154, 2007.
[24] J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking,” Proc. 27th ACM/IEEE Conf. Design Automation, pp.4651, 1990.
[25] Y. Matsunaga, P.C. McGeer, and R.K. Brayton, “On Computing the Transitive Closure of a State Transition Relation,” Proc. 30th Int'l Conf. Design Automation, pp.260265, 1993.
[26] R. Wimmer, M. Herbstritt, and B. Becker, “Optimization Techniques for BDDBased Bisimulation Minimization,” Proc. 17th ACM Great Lakes Symp. VLSI, pp.405410, 2007.
[27] M. Herbstritt, R. Wimmer, T. Peikenkamp, E. Böde, H. Hermanns, S. Johr, M. Adelaide, and B. Becker, “Analysis of Large SafetyCritical Systems: A Quantitative Approach,” SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 8, 2006, http:/www.avacs.org, 2009.
[28] R. Wimmer, M. Herbstritt, and B. Becker, “Minimization of Large State Spaces Using Symbolic Branching Bisimulation,” Proc. IEEE Work. Design and Diagnostics of Electronic Circuits and Systems, pp.712, 2006.
[29] R.E.A. Khayari, R. Sadre, and B.R. Haverkort, “Fitting WorldWide Web Request Traces with the EMAlgorithm,” Performance Evaluation, vol. 52, nos.23, pp.175191, 2003.
[30] A. Thümmler, P. Buchholz, and M. Telek, “A Novel Approach for Fitting Probability Distributions to Real Trace Data with the EM Algorithm,” Proc. Int'l Conf. Dependable Systems and Networks, pp.712721, 2005.
[31] M.F. Neuts, MatrixGeometric Solutions in Stochastic Models: An Algorithmic Approach. Dover, 1981.
[32] C. Commault and J.P. Chemla, “On Dual and Minimal PhaseType Representations,” Comm. Statistics: Stochastic Models, vol. 9, no. 3, pp.421434, 1993.
[33] M.A. Johnson and M.R. Taaffe, “The Denseness of Phase Distributions,” Purdue School of Industrial Eng. Research Memoranda 8820, Purdue Univ., 1988.
[34] S. Asmussen, O. Nerman, and M. Olsson, “Fitting PhaseType Distributions via the EM Algorithm,” Scandinavian J. Statistics, vol. 23, no. 4, pp.419441, 1996.
[35] A. Horváth and M. Telek, “Phfit: A General PhaseType Fitting Tool,” Proc. 12th Int'l Conf. Computer Performance Evaluation, Modeling Techniques and Tools, vol. 2324, pp.8291, 2002.
[36] R. Pulungan and H. Hermanns, “Orthogonal Distance Fitting for PhaseType Distributions,” SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 10, 2006, http:/www.avacs.org, 2009.
[37] J. Abate, G. Choudhury, and W. Whitt, “Calculation of the GI/G/1 Waiting Time Distribution and Its Cumulants from Pollaczek's Formulas,” Archiv für Elektronik und ÜBertragungstechnik, vol. 47, nos.5/6, pp.311321, 1993.
[38] K. Mitchell, J. Place, and A. van de Liefvoort, “Analytic Modeling with Matrix Exponential Distributions,” Simulation Councils Proc. Series, vol. 28, no. 1, pp.201204, 1996.
[39] H. Hermanns and J.P. Katoen, “Automated Compositional Markov Chain Generation for a PlainOld Telephone System,” Science of Computer Programming, vol. 36, pp.97127, 2000.
[40] BCG_MIN, “Project Website,” http://www.inrialpes.fr/vasy/cadp/manbcg_min.html ., Jan. 2008.
[41] H.A. Hansson, Time and Probability in Formal Design of Distributed Systems. Elsevier Science Inc., 1994.
[42] C. Baier, B.R. Haverkort, H. Hermanns, and J.P. Katoen, “ModelChecking Algorithms for ContinuousTime Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp.524541, June 2003.
[43] “System Requirements Specification—Chapter 2—Basic System Description,” technical report, Alcatel, Alston, Ansaldo Signal, Bombardier, Invensys Rail, Siemens, 2002.