The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - March/April (2009 vol.35)
pp: 274-292
Eckard Böde , OFFIS Institute for Information Technology, Oldenburg
Marc Herbstritt , Albert-Ludwigs-University, Freiburg im Breisgau
Holger Hermanns , Saarland University, Saarbrücken
Sven Johr , Saarland University, Saarbrücken
Thomas Peikenkamp , OFFIS Institute for Information Technology, Oldenburg
Reza Pulungan , Saarland University, Saarbrücken
Jan Rakow , Carl von Ossietzky University, Oldenburg
Ralf Wimmer , Albert-Ludwigs-University, Freiburg im Breisgau
Bernd Becker , Albert-Ludwigs-University, Freiburg im Breisgau
ABSTRACT
Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modelling tools like Statemate support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of Statemate enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high-speed train signalling system where the tool has been applied successfully.
INDEX TERMS
Real-time and embedded systems, Fault tolerance, Modeling techniques, Reliability, availability, and serviceability, Model checking, Reliability, Design notations and documentation, State diagrams
CITATION
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. 274-292, March/April 2009, doi:10.1109/TSE.2008.102
REFERENCES
[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.441-444, 2006.
[4] C. Baier, H. Hermanns, J.-P. Katoen, and B.R. Haverkort, “Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes,” Theoretical Computer Science, vol. 345, no. 1, pp.2-26, 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.167-178, 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.718-728, 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.477-492, 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.125-140, 2008.
[11] R.J. van Glabbeek and W.P. Weijland, “Branching Time and Abstraction in Bisimulation Semantics,” J. ACM, vol. 43, no. 3, pp.555-600, 1996.
[12] N. Wolovick and S. Johr, “A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes,” Proc. Fourth Int'l Conf. Formal Modeling and Analysis of Timed Systems, vol. 4202, pp.352-367, 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.293-333, 1996.
[15] D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, 1998.
[16] W. Damm, B. Josko, H. Hungar, and A. Pnueli, “A Compositional Real-Time Semantics of STATEMATE Designs,” Revised Lectures Int'l Symp. Compositionality: The Significant Difference, pp.186-238, 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.243-244, 2005.
[18] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[19] R.K. Brayton, G.D. Hachtel, A.L. Sangiovanni-Vincentelli, 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.99-113, 2003.
[22] A. Bouali and R. de Simone, “Symbolic Bisimulation Minimization,” Proc. Fourth Int'l Work Computer Aided Verification, pp.96-108, 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.139-154, 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.46-51, 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.260-265, 1993.
[26] R. Wimmer, M. Herbstritt, and B. Becker, “Optimization Techniques for BDD-Based Bisimulation Minimization,” Proc. 17th ACM Great Lakes Symp. VLSI, pp.405-410, 2007.
[27] M. Herbstritt, R. Wimmer, T. Peikenkamp, E. Böde, H. Hermanns, S. Johr, M. Adelaide, and B. Becker, “Analysis of Large Safety-Critical 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.7-12, 2006.
[29] R.E.A. Khayari, R. Sadre, and B.R. Haverkort, “Fitting World-Wide Web Request Traces with the EM-Algorithm,” Performance Evaluation, vol. 52, nos.2-3, pp.175-191, 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.712-721, 2005.
[31] M.F. Neuts, Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach. Dover, 1981.
[32] C. Commault and J.P. Chemla, “On Dual and Minimal Phase-Type Representations,” Comm. Statistics: Stochastic Models, vol. 9, no. 3, pp.421-434, 1993.
[33] M.A. Johnson and M.R. Taaffe, “The Denseness of Phase Distributions,” Purdue School of Industrial Eng. Research Memoranda 88-20, Purdue Univ., 1988.
[34] S. Asmussen, O. Nerman, and M. Olsson, “Fitting Phase-Type Distributions via the EM Algorithm,” Scandinavian J. Statistics, vol. 23, no. 4, pp.419-441, 1996.
[35] A. Horváth and M. Telek, “Phfit: A General Phase-Type Fitting Tool,” Proc. 12th Int'l Conf. Computer Performance Evaluation, Modeling Techniques and Tools, vol. 2324, pp.82-91, 2002.
[36] R. Pulungan and H. Hermanns, “Orthogonal Distance Fitting for Phase-Type 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.311-321, 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.201-204, 1996.
[39] H. Hermanns and J.-P. Katoen, “Automated Compositional Markov Chain Generation for a Plain-Old Telephone System,” Science of Computer Programming, vol. 36, pp.97-127, 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, “Model-Checking Algorithms for Continuous-Time Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp.524-541, June 2003.
[43] “System Requirements Specification—Chapter 2—Basic System Description,” technical report, Alcatel, Alston, Ansaldo Signal, Bombardier, Invensys Rail, Siemens, 2002.
20 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool