by Francesco Flammini, Nicola Mazzocca and Valeria Vittorini
Modern critical computer systems are rapidly growing in complexity. As a consequence, novel frameworks are needed to support multi-paradigm modelling for the dependability evaluation of such systems. OsMoSys (Object-based multi-formalism modelling of systems) is one of the latest projects in this category, whose originality consists in supporting certain aspects of object orientation and in the model analysis.
Safety-critical computer systems are becoming increasingly large, distributed and heterogeneous. This is one of the reasons why industry best practice for high-integrity systems rarely follows the correctness-by-design paradigm. When this happens, the approach involves just small subsystems, which need to be integrated to constitute the final system. It is well known that dependability attributes correspond to properties of the whole system, meaning a system-level analysis is needed to demonstrate compliance with the required targets. In system development or verification stages, model-based dependability prediction is a fundamental aspect of critical systems engineering. Model-based approaches are needed both to demonstrate safety-related properties (eg by model-checking or theorem-proving) and to evaluate quantitative attributes (eg mean time to failure, hazard rate) of the system.
Recently, new approaches are being investigated for the software engineering of critical systems. One of these follows the paradigm introduced by the Unified Modelling Language (MDE, Model-Driven Engineering). In practice, however, this is mostly used 'as a sketch', that is to say for documentation or informal verification purposes (though a formal specification of UML for real-time systems exists and several techniques have been proposed for a comprehensive dependability analysis of UML views).
In order to master the increasing complexity of modern control systems, modular and compositional approaches have been researched by the scientific community that allow engineers to adopt the modelling formalism most appropriate to the aspect of the system to be modelled (both hardware and software). All the components are then integrated into a single cohesive model of the whole system in order to evaluate system-level dependability attributes.
An attempt has been made to include these aspects in the theoretical framework of multi-paradigm modelling, which includes:
- Meta-Modelling, which is the process of modelling formalisms.
- Model Abstraction, concerned with the relationship between models at different levels of abstraction.
- Multi-Formalism modelling, concerned with the coupling of and transformation between models described in different formalisms.
The objective of the aforementioned techniques is to obtain a trade-off between ease of use, expressive power and solving efficiency. The explicit use of more formalisms requires that heterogeneous models be interconnected by means of proper operators, which can provide a mechanism for the interchange of results (connection) or the sharing of state, actions or events (composition). The art of manipulating models has only recently been extensively studied, and is sometimes given the name of model engineering (not to be confused with MDE). Model engineering also involves multi-level modelling modelling at different abstraction levels and multi-layer modelling the hierarchical modelling of different aspects of the same system, possibly including non-technological ones such as man-machine interaction.
An example scheme for the multi-paradigm modelling of a complex railway control system is illustrated in Figure 1. Each subsystem (on-board, lineside and trackside) has been divided into three layers, and all the sub-models are interconnected by means of intra/inter-layer and intra/inter-subsystem composition operators.
While multi-paradigm approaches allow engineers to govern modelling complexity, this is not the only complexity that needs to be reduced. Even though multi-formalism frameworks can hide from the modeller the complexity of the solving process, issues related to efficiency must be taken into account in model evaluation and model checking when dealing with large and stiff models.
There are two main (non-contrasting) ways of tackling efficiency issues. One is related to methodological aspects (divide-et-impera/iterative approaches, model abstraction, model transformation, model folding, flow-equivalent sub-models etc), while the other is related to technological means (eg distributed multi-solution on GRID systems).
All the aforementioned needs have been taken into account in the definition of the OsMoSys Modelling Methodology (OMM), which is implemented by the OsMoSys Multi-solution Framework (OMF). OsMoSys supports meta-modelling, some aspects of object-orientation (ie inheritance and polymorphism) and is built on a workflow-based orchestration of (possibly existing) solvers and external applications in order to achieve the multi-solution process. The OMF features a graphical user interface with which to draw models and retrieve results. Both formalisms and models are expressed in the OMF using the eXtended Markup Language (XML). The OMF supports both explicit and implicit multi-formalism: in the latter, a single formalism (eg repairable fault tree) is shown to the modeller, but more formal languages (eg generalized stochastic Petri nets, Bayesian networks) are used for model solution.
OsMoSys is the result of a multi-year inter-university research project, which has involved researchers from the Universities of Naples and Turin, together with engineers of Ansaldo STS (a railway systems supplier). It has been applied to the dependability (particularly maintainability, performability and safety) modelling of several critical computer-based systems, especially in the railway domain. The OMM is also suited to the modelling of complex biological systems and critical infrastructure security.
The development of the OMF is a work in progress, with additional modules becoming necessary to wrap solvers for new formalisms and to support new multi-solution paradigms. Future work will be aimed at the inclusion of additional composition operators into the framework and in the application of the OMM to new real-world case studies.
Links:
OsMoSys project page in Seclab research group Web site:
http://www.seclab.unina.it/
International Journal of Critical Computer-Based Systems:
http://www.inderscience.com/ijccbs
Please contact:
Francesco Flammini
ANSALDO STS Italy and University of Naples Federico II, Italy
E-mail: frflammi
unina.it
