Abstract
At the requirements level, formal verification and analysis are the focus of task’s attention which is develo** complex systems by formal methods. Model checking is a technique for analysis and automated verification of complex safety-critical software systems. In this paper, a requirement model verification method based on formal technology is proposed to practice the model checking activity into the development process. Firstly, this essay analyzes syntax and semantics of models, which are defined by tabular expressions in VRM (variables relationship model). Then we preprocess the VRM model to classify into events tables, conditions tables and model class tables, and transform the VRM model into the automaton state transfer diagram with the help of semantic complementary work. Finally, we design an automatic model transformation framework from the VRM model to the model verification tool (nuXmv) and implement a translator between the formal specification language VRM and the symbolic model checker nuXmv. In this paper, we discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bernardeschi, C., Cassano, L., Domenici, A.: SRAM-based FPGA systems for safety-critical applications: a survey on design standards and proposed methodologies. J. Comput. Sci. Technol. 30(2), 373–390 (2015)
Biernacki, J.: Alvis models of safety critical systems state-base verification with nuXmv. In: Computer Science & Information Systems, pp. 1701–1708 (2016)
Cook, B., Khlaaf, H., Piterman, N.: Verifying increasingly expressive temporal logics for infinite-state systems. J. Acm 64(2), 1–39 (2017)
Hu, J., Hu, J., Wang, W., Kang, J., Gao, Z.: Constructing formal specification models from domain specific natural language requirements. In: 2020 6th International Symposium on System and Software Reliability (ISSSR), pp. 52–60 (2020)
King, J.M., Bergeron, C.A., Taylor, C.E.: Finite state machine implementation for left ventricle modeling and control. BioMed. Eng. OnLine 18(1), 1–24 (2019)
Parr, J.B.: ANTLRworks: an ANTLR grammar development environment. Softw. Pract. Experience 38(12), 1305–1332 (2010)
Rauzy, A.B., Haskins, C.: Foundations for model-based systems engineering and model-based safety assessment. Syst. Eng. 22(2), 146–155 (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Zhang, Y., Hu, J., Wang, L., Gu, Q., Rong, H. (2022). Formal Verification for VRM Requirement Models. In: Liang, Q., Wang, W., Liu, X., Na, Z., Zhang, B. (eds) Communications, Signal Processing, and Systems. CSPS 2021. Lecture Notes in Electrical Engineering, vol 878. Springer, Singapore. https://doi.org/10.1007/978-981-19-0390-8_121
Download citation
DOI: https://doi.org/10.1007/978-981-19-0390-8_121
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-19-0389-2
Online ISBN: 978-981-19-0390-8
eBook Packages: EngineeringEngineering (R0)