The graphical modelling languages UML and SysML, nowadays widely used in industry, integrate different modelling concepts and notations in one standardised framework. However, they lack a clearly defined, unambiguous semantics and thus their formal verification represents a challenge. On the other hand, current safety standards, including ISO 26262, demand such verification especially for safety-relevant systems. The literature proposes a plethora of different semantics and formalisms for UML/SysML. In this paper we compare and summarise existing work on the formalisation of behavioural UML and SysML models and their verification. Our goal is to foster a better understanding of the problems related to UML/SysML formalisation, and to aid people bridging the gap from high level graphical modelling to formal verification techniques.

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.

Continuous-time Markov decision processes (CTMDPs) are behavioral models with continuous-time, nondeterminism and memoryless stochastics. Recently, an efficient timed reachability algorithm for CTMDPs has been presented, allowing one to quantify, e. g., the worst-case probability to hit an unsafe system state within a safety critical mission time. This algorithm works only for uniform CTMDPs -- CTMDPs in which the sojourn time distribution is unique across all states. In this paper we develop a compositional theory for generating CTMDPs which are uniform by construction. To analyze the scalability of the method, this theory is applied to the construction of a fault-tolerant workstation cluster example, and experimentally evaluated using an innovative implementation of the timed reachability algorithm. All previous attempts to model-check this seemingly well-studied example needed to ignore the presence of nondeterminism, because of lacking support for modelling and analysis.