@article{citeulike:4414144,
    author = {Bode, E. and Herbstritt, M. and Hermanns, H. and Johr, S. and Peikenkamp, T. and Pulungan, R. and Rakow, J. and Wimmer, R. and Becker, B.},
    title = {Compositional Dependability Evaluation for STATEMATE},
    journal = {IEEE Transactions on Software Engineering},
    number = {2},
    pages = {274--292},
    priority = {2},
    volume = {35},
    year = {2009},
    access={restricted},
    subprojects={S3},
    bibtex={boede.jse09.bib},
    pdf={boede.jse09.pdf},
    keywords = {checking, ctmc, mdp, model, stochastic},
    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.},
}