Model-based dependability evaluation is challenging and therefore prone to error, especially if one uses lower-level formalisms such as Markov Chains, Stochastic Petri Nets or Stochastic Process Algebra (SPA). For that reason, in an industrial environment mainly high-level specification formalisms such as AADL, UML or SysML are employed. Those languages mostly lack formal semantics and capabilities to model stochasticity which is an intrinsic characteristic of dependable systems.
Dependability Analysis using LARES
For the purpose of bridging the gap between high-level formalisms and formal modelling languages, the LAnguage for REconfigurable dependable Systems (LARES) regarding its syntax and semantics has been developed. It can serve both as an intermediate lan- guage and as a stand-alone modelling formalism. LARES provides language elements for hierarchical modelling. It separates between structure and behaviour. Furthermore, it introduces scopes which restrict the visibility of definitions and named statements in order to facilitate structured model descriptions. The semantics of LARES is given by means of SPA and labelled transition systems (LTS). For this purpose, two transformations have been realised which can fully automatically map a LARES model to either its SPA equivalent or directly to an LTS. A number of implementations constitute the LARES modelling environment: The editor component supports syntax highlighting and code completion. It also checks context conditions in order to ensure model validity. The analysis component carries out the transformations of a given model and allows visualising the constructed instance tree, the composed state space or the calculated dependability measures. And finally, among other things, the library implements language definitions, parsers, transformations and bindings to external solvers. Both transformations can be ver- ified as the resulting SPA model and the LTS have to correspond regarding their behaviour.