Assurance Cases (ACs) are methods to justify system confidence in essential properties such as safety, reliability, etc. But the manual generation of AC is time-consuming and prone to errors. Also, AC update during the entire system life cycle calls for more labour. Thus, Model-based Engineering (MBE) techniques are well exploited for an automatic process of AC generation. We propose an AC generation approach using Epsilon to tackle the automation of the AC process.
Hawkins et al. [1] used the model weaving [2] to establish the mapping between system models and AC elements at the metamodel level. The AC is generated by automatic pattern instantiation. An advantage is that the system models are extracted and instantiated automatically. Gacek et al. [3] query AADL system models to generate AC models. The query environment is integrated with AADL modelling platform. In the work of ˇ Sljivo et al. [4], ACs are derived from system design pattern instead of generating AC directly from system model. Gallina and Nyberg [5] also generate AC by model query technique. The queried models are the system data (e.g., verification plan) compliant with OSLC standard (Open Services for Lifecycle Collaboration) [6]. Denney and Pai [7] construct a complete AC by automatic pattern instantiation. The system design data are not required to be models.
To realize the AC generation using MBE, Model transformation and model query are the key techniques used in the above work.
Model query and transformation is the heart of MBE. In many domains such as railway, automotive, business process engineering, and embedded systems, models are key to success in modern engineering processes [8]. Due to the complexity of the systems, there is a strong need for model-to-model, model-to-text transformation techniques, and particularly model-to-model model transformations [8]. There are three types of model transformation languages: declarative, imperative and hybrid [9]. The declarative transformation languages are more suitable for scenarios where the source and target metamodels are similar to each other in terms of structure and organization. However, such languages are not suitable for significant sequential processing and complex mappings. The imperative transformation languages address a wider range of transformation scenarios, and typically operate at a low level of abstraction. So the users need to manually address issues such as tracing, resolving target elements with their source counterparts, and orchestrating the transformation execution. Hybrid languages provide a declarative rule-based execution scheme as well as imperative features for handling complex transformation scenarios [10].
Model transformation is only one of the many tools in a model engineering toolkit. Automated support of other model management such as model comparison, merging, validation, etc., is as essential as model transformation. However, many of the model transformation languages lack integration with other model management support [10]. There are a large number of transformation languages, we assess here some widely-used and actively developed languages include QVT, ATL, Kermeta, and XTend, and Epsilon.
Kermeta [11] is a transformation language of the openArchitectureWare framework. It adopts a different approach to model management by providing a general-purpose imperative language to perform all model management tasks. However, it is a purely imperative.
XTend is also an imperative language of the openArchitectureWare framework, therefore “requires the user to implement transformation rules, scheduling and support for traceability almost from scratch for each transformation” [10]. However, XTend is integrated with other model management languages of the openArchitectureWare framework for code generation and model validation.
Query/View/Transformation (QVT) [12] is a hybrid declarative/imperative transformation languages published as an OMG standard. With regards to the support of model management, the OMG has also standardized a model-to-text transformation language which reuses parts of QVT.
ATLAS Transformation Language (ATL) is a domain-specific hybrid language widely used for specifying model-to-model transformations [13]. It is a part of the ATLAS Model Management Architecture (AMMA) platform [14]. ATL is inspired by the OMG QVT requirements and builds upon the OCL formalism. Moreover, it has been shown that ATL can be used to perform model validation and merging to a certain extent.
Epsilon Transformation Language (ETL) is a hybrid model transformation language. It has been developed atop the infrastructure provided by the Epsilon model management platform. Epsilon, standing for Extensible Platform of Integrated Languages for Model Management, is a platform for building consistent and interoperable task-specific languages for model management tasks such as model transformation, code generation, model comparison, merging, refactoring and validation [15]. Therefore, ETL is integrated with other languages which are capable of model validation, model comparison, model merging etc. provided by Epsilon [10]. And this is the advantage of ETL comparing with most of other transform languages that have no or less support of the model manipulation capability.
Fig.1 Epsilon languages structure [16]
We propose an AC generation approach using Epsilon [10] for model query, transformation, etc. Thus, the generated AC models can further be managed with MBE capabilities, such as review by query, comparison for update. Our approach is shown in Fig. 2.
Fig.2 AC generation approach using Epsilon [17]
System development process produces the system data of any format, including models (e.g., EMF models), and unstructured data (such as spreadsheet, text, etc.). For the automation of AC pattern instantiation, we first process the unstructured data into models backed by predesigned metamodels. Then, AC models are created by querying system models (hazard analysis, system models, etc.) . The query rules are predefined for claims of different scenarios, and stored in a library for reuse. The AC models shall be furtherly integrated into a complete module. For the claims to be verified by formal methods (FM), formal assertions are generated from the safety requirement that are used to generate these claims. The textual requirements will be rewritten with a Controlled Natural Language (CNL), and converted into a structured format, such as XML. The assertion templates shall be defined according to the target FM tools. The formal assertions will be generated automatically by model-to-text transformation. The formal verification results are obtained to create the AC evidence models by model transformation. The last step is to integrate the evidence models in to the AC module [17].
Our approach is inspired by and expands [1] to cover not only system design models but also the unstructured data such as hazard analysis result. We refer the model query concept in [3] at design model level. The difference is that our approach has no constraint on system modelling languages and is capable of assembling with AC structure generated from other sources [17]. More details about the proposal can be found in [17].
References
[1] R. Hawkins, I. Habli, D. Kolovos, R. Paige, and T. Kelly, “Weaving an Assurance Case from Design: A Model-Based Approach,” in 2015 IEEE 16th International Symposium on High Assurance Systems Engineering. IEEE, 2015, pp. 110–117.[2] M. D. Del Fabro, J. B´ezivin, and P. Valduriez, “Weaving models with the eclipse amw plugin,” in Eclipse Modeling Symposium, Eclipse Summit Europe, vol. 2006, 2006, pp. 37–44.
[3] A. Gacek, J. Backes, D. Cofer, K. Slind, and M. Whalen, “Resolute: an assurance case language for architecture models,” in ACM SIGAda Ada Letters, vol. 34, no. 3. ACM, 2014, pp. 19–28.
[4] I. ˇ Sljivo, G. J. Uriagereka, S. Puri, and B. Gallina, “Guiding assurance of architectural design patterns for critical applications,” Journal of Systems Architecture, vol. 110, p. 101765, 2020.
[5] B. Gallina and M. Nyberg, “Pioneering the creation of iso 26262-compliant oslc-based safety cases,” in 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE, 2017, pp. 325–330.
[6] “Open Services for Lifecycle Collaboration.” http://open-services.net/, online; accessed 15th December, 2021.
[7] E. Denney and G. Pai, “Tool support for assurance case development,” Automated Software Engineering, vol. 25, no. 3, pp. 435–499, 2018.
[8] A. Bucchiarone, J. Cabot, R. F. Paige, and A. Pierantonio, “Grand challenges in model-driven engineering: an analysis of the state of the research,” Softw. Syst. Model., pp. 1–9, 2020.
[9] K. Czarnecki and S. Helsen, “Classification of Model Transformation Approaches,” pp. 1–17.
[10] Kolovos, Dimitrios S., Richard F. Paige, and Fiona AC Polack. “The epsilon transformation language.” In International Conference on Theory and Practice of Model Transformations, pp. 46-60. Springer, Berlin, Heidelberg, 2008.
[11] F. Chauvel and F. Fleurey, “Kermeta Language Overview.” 2007.
[12] Object Management Group (OMG), “MOF Query/View/Transformation Version:1.3,” 2016. [Online]. Available: https://www.omg.org/spec/QVT/About-QVT/.
[13] F. Jouault, F. Allilaire, J. Bézivin, and I. Kurtev, “ATL : A model transformation tool,” vol. 72, pp. 31–39, 2008.
[14] J. Bézivin, F. Jouault, P. Rosenthal, and P. Valduriez, “Modeling in the large and modeling in the small,” in Model Driven Architecture, Springer, 2004, pp. 33–46.
[15] D. D. Kolovos, L. Rose, R. Paige, and A. García-domínguez, “The Epsilon book,” 2010.
[16] Model Driven Engineering lecture, University of York, 2019.
[17] Generation and verification of executable assurance case by model-based engineering. In 2021 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE. Preprint: https://eprints.whiterose.ac.uk/179470/1.
About the Author: Fang Yan
Fang has her bachelor’s degree in Electronic and Information Engineering at the Civil Aviation University of China and completed her master’s degree in Ecole National Superieur D’ingeneurs De Constructions Aeronautiques. After the university, she worked as a lecturer in a university and had 7 years of part-time experience in aviation certification in terms of system safety and software safety. She has her interest in safety methodology for autonomous systems and chose to continue in academia and therefore into this PhD.
