An ANTLR-based Flattening Framework for AltaRica 3.0 Model

doi:10.23940/ijpe.19.09.p20.24622475

Int J Performability Eng ›› 2019, Vol. 15 ›› Issue (9): 2462-2474.doi: 10.23940/ijpe.19.09.p20.24622475

Previous Articles Next Articles

An ANTLR-based Flattening Framework for AltaRica 3.0 Model

Jun Hu^a,c, Shuo Chen^a,c,*, Defeng Chen^d, Jiexiang Kang^b, and Hui Wang^b

^aCollege of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, 211106, China;
^bDepartment of Software, China National Aeronautic Radio Electronics Research Institute, Shanghai, 200233, China;
^cCollaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing, 210007, China;
^dSchool of Mechanical Engineering, Hefei University of Technology, Hefei, 230601, China

Submitted on ; Revised on ; Accepted on
Contact: *. Shuo Chen is a master's candidate at Nanjing University of Aeronautics and Astronautics. His research interests include software analysis and system safety analysis. E-mail address: nuaa_cs@163.com
About author:Jun Hu received his Ph.D. degree in computer software and theory from Nanjing University in 2006. He is an associate professor at Nanjing University of Aeronautics and Astronautics. His research interests include model-based safety analysis, software analysis, and formal methods. Defeng Chen is a student at Hefei University of Technology. His research interests include machine learning and robot engineering. Jiexiang Kang is a researcher at China National Aeronautic Radio Electronics Research Institute. His research interests include avionics technology, software engineering, and embedded operating systems. Hui Wang is a senior engineer at China National Aeronautic Radio Electronics Research Institute. Her research interests include software engineering and software verification

Abstract

Abstract: AltaRica is a modeling language that is capable of hierarchical modelling and fault behavior description for industrial safety-critical system design. AltaRica 3.0 is the latest version, and its semantics are based on a formal GTS (Guarded Transition Systems) model. One of the key steps in the process of safety analysis toward AltaRica 3.0 models is that how to flatten a hierarchical AltaRica 3.0 model into a semantically equivalent GTS semantic model. This paper proposes an AltaRica 3.0 model flattening algorithm framework based on ANTLR (Another Tool for Language Recognition). Firstly, considering the different structural features of Block and Class, the AltaRica 3.0 model is sliced carefully in order to obtain the corresponding AST (Abstract Syntax Tree). Secondly, a set of recursive transformation algorithms are designed to extract and transform the AltaRica model elements, which are stored in the AST nodes based on the traversal technique of the AST. Then, a semantically equivalent flattened GTS model can be obtained. Lastly, several case studies show that the algorithms designed in this paper can effectively implement the flattening process of AltaRica 3.0 models.

Key words: ANTLR, AltaRica 3.0, flattening, AST, A2GTS, transition algorithm

Jun Hu, Shuo Chen, Defeng Chen, Jiexiang Kang, and Hui Wang. An ANTLR-based Flattening Framework for AltaRica 3.0 Model [J]. Int J Performability Eng, 2019, 15(9): 2462-2474.

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

References

1. L. Zhongwen and X. Guang, “Formal Method and Safety Critical System,”Journal of Computer Applications, Vol. 20, pp. 36-38, 2000
2. C. Che and F. Liu, “Research on Model based Safety Analysis,”Advances in Aeronautical Science and Engineering, Vol. 7, pp. 369-373, 2016
3. A. Gomes, A. Mota, A. Sampaio, F. Ferri,J. Buzzi, “Systematic Model-based Safety Assessment via Probabilistic Model Checking,”Lecture Notes in Computer Science, Vol. 6415, pp. 625-639, 2010
4. M. Sango, F. Vallée, A. C. Vié, J. L. Voirin, X. Leroux,V. Normand, “MBSE and MBSA with Capella and Safety Architect Tools,” inProceedings of International Conference on Complex Systems Desigh and Management, pp. 239, 2016
5. L. Kloul, T. Prosvirnova,A. Rauzy, “Modeling Systems with Mobile Components: A Comparison Between AltaRica and PEPA Nets,”Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, Vol. 227, pp. 599-613, 2013
6. A. Arnold, G. Point, A. Griffault,A. Rauzy, “The AltaRica Formalism for Describing Concurrent Systems,”Fundamenta Informaticae, Vol. 40, pp. 109-124, 1999
7. W. Zhipeng, H. Jun, C. Song,S. Jiaojie, “Safety Verification Methodology of Embedded System based on AltaRica Model,”Journal of Frontiers of Computer Science and Technology, Vol. 11, pp. 24-36, 2017
8. T. Prosvirnova and A. Rauzy, “AltaRica 3.0 Project: Compile Guarded Transition Systems into Fault Trees,” in Proceedings of European Safety and Reliability Conference, ESREL, 2013
9. A. B. Rauzy, “Guarded Transition Systems: A New States/Events Formalism for Reliability Studies,”Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, Vol. 222, pp. 495-505, 2008
10. D. A. Levin, Y. Peres,E. L. Wilmer, “Markov Chains and Mixing Times, ” American Mathematical Society, 2009
11. M. Bozzano, A. Cimatti, O. Lisagor, C. Mattarei, S. Mover, M. Roveri, et al., “Safety Assessment of AltaRica Models via Symbolic Model Checking,”Science of Computer Programming, Vol. 98, pp. 464-483, 2015
12. G. Point and A. Rauzy, “AltaRica: Constraint Automata as a Description Language,”Journal Europeen des Systèmes Automatisés, Vol. 33, pp. 1033-1052, 1999
13. A. Cimatti, E. Clarke, F. Giunchiglia,M. Roveri, “NUSMV: A New Symbolic Model Checker,”International Journal on Software Tools for Technology Transfer, Vol. 2, pp. 410-425, 2000
14. M. Boiteau, Y. Dutuit, A. Rauzy,J. P. Signoret, “The AltaRica Data-Flow Language in Use: Modeling of Production Availability of a Multi-State System,”Reliability Engineering and System Safety, Vol. 91, pp. 747-755, 2006
15. A. Arnold, G. Point, A. Griffault,A. Rauzy, “The AltaRica Formalism for Describing Concurrent Systems,”Fundamenta Informaticae, Vol. 40, pp. 109-124, 1999
16. A. Griffault and A. Vincent, “The Mec 5 Model-Checker,” inProceedings of International Conference on Computer Aided Verification, pp. 488-491, 2004
17. T. Prosvirnova, M. Batteux, P. Brameret, A. Cherfi, T. Friedlhuber, J. Roussel, et al., “The Altarica 3.0 Project for Model-based Safety Assessment,”IFAC Proceedings Volumes, Vol. 46, pp. 127-132, 2013
18. X. Ni-zhou and W. Li-song, “Safety Analysis for Avionics System based on Model Driven,”Computer and Modernization, pp. 21-26, 2015
19. F. K. Zhang, Y. F. He,Q. F. Gu, “A Model-based Safety Analysis Method for Head-up Display System,”Avionics Technology, pp. 52-56, 2014
20. T. Prosvirnova and A. Rauzy, “Guarded Transition Systems: Pivot Modelling Formalism for Safety Analysis,”Actes du Congres Lambda-Mu, 2012
21. R. W. Quong, “ANTLR: A Predicated-LL(k) Parser Generator,”Software Practice and Experience, Vol. 25, pp. 789-810, 2010
22. T. Parr, “The Definitive ANTLR 4 Reference, ” Pragmatic Bookshelf, 2013
23. T. Prosvirnova, “AltaRica 3.0: A Model-based Approach for Safety Analyses,” Ecole Polytechnique, 2014
24. P. Arcaini, A. Gargantini,E. Riccobene, “A Model Advisor for NuSMV Specifications,”Innovations in Systems and Software Engineering, Vol. 7, pp. 97-107, 2011
25. G. Holzmann, “Spin Model Checker, the: Primer and Reference Manual,” Addison-Wesley, Boston, 2004
26. S. Li and D. Su, “A Practicable MBSA Modeling Process using Altarica, ” inProceedings of International Symposium on Model-based Safety and Assessment, pp. 1-13, 2014
27. J. Hu, S. Chen,M. M. Wang, “A Transformation Method for AltaRica3.0 to Promela and Its verification,”Computer Engineering and Science, Vol. 39, pp. 708-716, 2017
28. H. Mortada, T. Prosvirnova,A. Rauzy, “Safety Assessment of an Electrical System with AltaRica 3.0,” inProceedings of International Symposium on Model-Based Safety Conference, 2014

[1]	Aashita Rajput, Muskan Yadav, Sachin Yadav, Megha Chhabra, and Arun Prakash Agarwal. Patch-Based Breast Cancer Histopathological Image Classification using Deep Learning [J]. Int J Performability Eng, 2023, 19(9): 607-623.
[2]	Kanika Wadhwa, Shreshtha Singh, Arun Sharma, and Swaty Wadhwa. Machine Learning-Based Breast Cancer Prediction Model [J]. Int J Performability Eng, 2023, 19(1): 55-63.
[3]	Sagnik Pal, Rutvik Patel, Vijayasherly V., and Ramani Selvanambi. Hashtag Recommendation System for Instagram Posts using Transfer Learning with EfficientNet and ALS Model [J]. Int J Performability Eng, 2022, 18(8): 552-558.
[4]	Rajan Prasad Tripathi, Sunil Kumar Khatri, and Darelle Van Greunen. Relative Examination of Breast Malignant Growth Analysis Utilizing Different Machine Learning Algorithms [J]. Int J Performability Eng, 2022, 18(6): 417-425.
[5]	Jalaj Pateria, Laxmi Ahuja, and Subhranil Som. Critical Path to Place Decoys in Deception Biota [J]. Int J Performability Eng, 2022, 18(12): 854-862.
[6]	Sidali Bacha, Ahmed Bellaouar, Jean-Paul Dron, and Houssam Lala. Optimization of PM Intervals of an Oil Pump using a Generalized Proportional Intensity Model GPIM [J]. Int J Performability Eng, 2021, 17(7): 569-578.
[7]	Leila M. Bogdanova, Sergey Ya. Nagibin, and Alexander S. Chemakin. Analysis of the Criteria for Assessing the Forecast Quality of Industrial Safety Indicators of Enterprises [J]. Int J Performability Eng, 2021, 17(6): 519-527.
[8]	Yi-Hao Chiu, Yi-Kuei Lin, and Thi-Phuong Nguyen. Network Reliability of a Stochastic Online-Food Delivery System with Space and Time Constraints [J]. Int J Performability Eng, 2021, 17(5): 433-443.
[9]	S. Anbazhagan and Bhuvaneswari Ramachandran. Ameliorating Vertically Bundled Electricity Price Prediction Exclusively from ICMLP Network [J]. Int J Performability Eng, 2021, 17(4): 364-370.
[10]	Sambasivarao Kalepu and Ramanaiah Nallu. Optimization and Prediction of Mechanical Behavior of Nitinol-based Composites [J]. Int J Performability Eng, 2021, 17(11): 966-972.
[11]	Anita Agárdi, László Kovács, and Tamás Bányai. Using Time Series and Classification in Vehicle Routing Problem [J]. Int J Performability Eng, 2021, 17(1): 14-25.
[12]	Yong Yang. Wireless Sensor Node Location based on IGWO-LSSVM [J]. Int J Performability Eng, 2020, 16(9): 1434-1442.
[13]	Huaiguang Wu, Pengjie Xie, Ming Cheng, and Hongwei Tao. A Hybrid Model of Predicting Breast Cancer Survivability based on Specific Stages [J]. Int J Performability Eng, 2020, 16(8): 1183-1192.
[14]	Chunyu Lu and Shaojun Liu. Contact Fatigue Reliability Analysis of Rolling Bearing based on Elastohydrodynamic Lubrication [J]. Int J Performability Eng, 2020, 16(6): 855-865.
[15]	Laurent Bouillaut, Olivier François, Yves Putallaz, Clément Granier and Christophe Cieux. A Hybrid Approach for the Evaluation of Rail Monitoring and Maintenance Strategies for the Grand Paris Express New Metro [J]. Int J Performability Eng, 2020, 16(11): 1685-1697.

An ANTLR-based Flattening Framework for AltaRica 3.0 Model

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended 0