复杂嵌入式系统需求一致性的组合验证方法
作者:
中图分类号:

TP311


Compositional Verification for Requirements Consistency of Complex Embedded Systems
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [39]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    形式化方法在需求一致性验证领域已经取得了显著的成就. 然而, 随着嵌入式系统需求复杂度的不断提升, 需求一致性验证面临着状态空间过大的挑战. 为了有效约减验证的状态空间, 同时考虑到嵌入式系统需求所涉及的设备强依赖性, 提出一种复杂嵌入式系统需求一致性的组合验证方法. 它基于需求分解, 识别需求间的依赖关系, 通过这些依赖关系组装验证子系统, 从而实现对复杂嵌入式系统需求的组合验证, 并能初步定位到不一致的需求. 具体而言, 采用问题框架方法对需求进行建模和分解, 并预设领域设备知识库对设备的物理特性进行建模. 在验证子系统的组装过程中, 生成预期软件的行为模型, 并结合物理设备的模型进行动态组装. 最后, 采用航空领域机载侦查系统进行了实例研究, 验证了方法的可行性和有效性, 并通过5个案例评估证实了验证状态空间的显著减小. 此方法为复杂嵌入式系统需求的验证提供了一种切实可行的解决方案.

    Abstract:

    Formal methods have made significant strides in the field of requirements consistency verification. However, as the complexity of embedded system requirements continues to increase, verifying requirements consistency faces the challenge of dealing with an excessively large state space. To effectively reduce the verification state space, while also considering the strong dependency among devices in embedded system requirements, this study proposes a compositional verification method for ensuring the consistency of requirements in complex embedded systems. This method is based on requirement decomposition and identification of dependencies among requirements. By leveraging these dependencies, it assembles verification subsystems, enabling the compositional verification of complex embedded system requirements and facilitating the initial identification of inconsistencies. Specifically, the problem frames approach is employed for requirement modeling and decomposition, while a domain-specific device knowledge base is utilized for modeling the physical characteristics of devices. During the assembly of verification subsystems, models of expected software behavior are generated and dynamically integrated with physical device models. Finally, the feasibility and effectiveness of this method are validated through a case study of an airborne reconnaissance control system, demonstrating a significant reduction in the verification state space through five case evaluations. This method thus provides a practical solution for verifying the requirements of complex embedded systems.

    参考文献
    [1] 杨孟飞, 顾斌, 段振华, 金芝, 詹乃军, 董云卫, 田聪, 李戈, 董晓刚, 李晓锋. 嵌入式软件智能合成框架及关键科学问题. 中国空间科学技术, 2022, 42(4): 1–7.
    Yang MF, Gu B, Duan ZH, Jin Z, Zhan NJ, Dong YW, Tian C, Li G, Dong XG, Li XF. Intelligent program synthesis framework and key scientific problems for embedded software. Chinese Space Science and Technology, 2022, 42(4): 1–7 (in Chinese with English abstract).
    [2] Zowghi D, Gervasi V. On the interplay between consistency, completeness, and correctness in requirements evolution. Information and Software Technology, 2003, 45(14): 993–1009.
    [3] Chen XH, Zhong ZW, Jin Z, Zhang M, Li T, Chen X, Zhou TL. Automating consistency verification of safety requirements for railway interlocking systems. In: Proc. of the 27th Int’l Requirements Engineering Conf. Jeju: IEEE, 2019. 308–318.
    [4] 黄友能, 张鹏基, 侯晓鹏, 唐涛. 基于混成自动机的城市轨道交通ZC子系统建模与验证方法. 中国铁道科学, 2016, 37(2): 114–121.
    Huang YN, Zhang PJ, Hou XP, Tang T. Modeling and verification method of ZC subsystem in urban rail transit based on hybrid automata. China Railway Science, 2016, 37(2): 114–121 (in Chinese with English abstract).
    [5] Fotso SJT, Frappier M, Laleau R, Mammar A. Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. In: Proc. of the 6th Int’l Conf. on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Southampton: Springer, 2018. 262-276. [doi: 10.1007/978-3-319-91271-4_18]
    [6] 杨璐, 陈永刚. 基于MSC与UPPAAL的区域控制器切换场景建模与验证. 铁道标准设计, 2018, 62(5): 171–174, 179.
    Yang L, Chen YG. Modeling and verification of switch scene of zone controller based on MSC and UPPAAL. Railway Standard Design, 2018, 62(5): 171–174, 179 (in Chinese with English abstract).
    [7] Chen XH, Liu QQ, Mallet F, Li Q, Cai SB, Jin Z. Formally verifying consistency of sequence diagrams for safety critical systems. Science of Computer Programming, 2022, 216: 102777.
    [8] 李腾飞, 孙军峰, 吕新军, 陈祥, 刘静, 孙海英, 何积丰. 基于SMT的区域控制器同步反应式模型的形式化验证. 软件学报, 2023, 34(7): 3080–3098. http://www.jos.org.cn/1000-9825/6861.htm
    Li TF, Sun JF, Lü XJ, Chen X, Liu J, Sun HY, He JF. SMT-based formal verification of synchronous reactive model for zone controller. Ruan Jian Xue Bao/Journal of Software, 2023, 34(7): 3080–3098 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6861.htm
    [9] Vuotto S, Narizzano M, Pulina L, Tacchella A. Poster: Automatic consistency checking of requirements with ReqV. In: Proc. of the 12th IEEE Conf. on Software Testing, Validation and Verification (ICST). Xi’an: IEEE, 2019. 363–366. [doi: 10.1109/ICST.2019.00043]
    [10] Wang XB, Li CY, Zhao L. Requirement specification extraction and analysis based on propositional projection temporal logic. Journal of Software: Evolution and Process, 2024, 36(4): e2558.
    [11] Clarke EM, Long DE, McMillan KL. Compositional model checking. In: Proc. of the 4th Annual Symp. on Logic in Computer Science. Pacific Grove: IEEE, 1989. 353-362. [doi: 10.1109/LICS.1989.39190]
    [12] Vidal M, Massoni T, Ramalho F. A domain-specific language for verifying software requirement constraints. Science of Computer Programming, 2020, 197: 102509.
    [13] Chen XH, Zhang J, Jin Z, Zhang M, Li T, Chen X, Zhou TL. Empowering domain experts with formal methods for consistency verification of safety requirements. IEEE Trans. on Intelligent Transportation Systems, 2023, 24(12): 15146–15157.
    [14] Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W. UPPAAL—A tool suite for automatic verification of real-time systems. In: Proc. of the 1995 Int’l Hybrid Systems III. Berlin: Springer, 1995. 232-243. [doi: 10.1007/BFb0020949]
    [15] Massoni T, Mousavi MR. Formal Methods: Foundations and Applications. In: Proc. of the 20th Brazilian Symp. Salvador: Springer, 2018.
    [16] Pereira T, Ribeiro Q, Melo M, Magro S, Alencar F, Castro J. Requirements engineering for embedded systems: A systematic literature review. In: Proc. of the 2021 Workshop on Requirements Engineering (WER). 2021.
    [17] Yuan ZH, Chen XH, Liu J, Yu YJ, Sun HY, Zhou TL, Jin Z. Simplifying the formal verification of safety requirements in zone controllers through problem frames and constraint-based projection. IEEE Trans. on Intelligent Transportation Systems, 2018, 19(11): 3517–3528.
    [18] 刘筱珊, 袁正恒, 陈小红, 陈铭松, 刘静, 周庭梁. 区域控制器的安全需求建模与自动验证. 软件学报, 2020, 31(5): 1374–1391. http://www.jos.org.cn/1000-9825/5952.htm
    Liu XS, Yuan ZH, Chen XH, Chen MS, Liu J, Zhou TL. Safety requirements modeling and automatic verification for zone controllers. Ruan Jian Xue Bao/Journal of Software, 2020, 31(5): 1374–1391 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5952.htm
    [19] Jackson M. Software Requirements and Specifications: A Lexicon of Practice, Principles and Prejudices. New York: Addison-Wesley, 1995.
    [20] Jackson M. Problem Frames: Analyzing and Structuring Software Development Problems. Boston: Addison-Wesley, 2001.
    [21] Jin Z, Chen XH, Zowghi D. Performing projection in problem frames using scenarios. In: Proc. of the 16th Asia-Pacific Software Engineering Conf. Batu Ferringhi: IEEE, 2009. 249-256. [doi: 10.1109/APSEC.2009.22]
    [22] Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L. Rodin: An open toolset for modelling and reasoning in Event-B. Int’l Journal on Software Tools for Technology Transfer, 2010, 12(6): 447–466.
    [23] Rudolph E, Graubmann P, Grabowski J. Tutorial on message sequence charts. Computer Networks and ISDN Systems, 1996, 28(12): 1629–1641.
    [24] Caspi P, Pilaud D, Halbwachs N, Plaice JA. LUSTRE: A declarative language for real-time programming. In: Proc. of the 14th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. Munich: ACM, 1987. 178-188. [doi: 10.1145/41625.41641]
    [25] Younes HLS. Verification and planning for stochastic processes with asynchronous events [Ph.D. Thesis]. Schenley Park: Carnegie Mellon University, 2004.
    [26] Ramesh Y, Rao MVP. Statistical model checking for probabilistic temporal epistemic logics. In: Proc. of the 14th Int’l Conf. on Agents and Artificial Intelligence. Online: SciTePress, 2022. 53–63. [doi: 10.5220/0010847900003116]
    [27] Zhu WJ, Wu HM, Deng ML. LTL model checking based on binary classification of machine learning. IEEE Access, 2019, 7: 135703–135719.
    [28] Jhala1 R, McMillan KL. Microarchitecture verification by compositional model checking. In: Proc. of the 13th Int’l Conf. on Computer Aided Verification. Paris: Springer, 2001. 396–410. [doi: 10.1007/3-540-44585-4_40]
    [29] McMillan KL. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Proc. of the 11th IFIP WG 10.5 Advanced Research Working Conf. on Correct Hardware Design and Verification Methods. Livingston: Springer, 2001. 179–195. [doi: 10.1007/3-540-44798-9_17]
    [30] Namjoshi KS, Trefler RJ. Parameterized compositional model checking. In: Proc. of the 22nd Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Eindhoven: Springer, 2016. 589–606. [doi: 10.1007/978-3-662-49674-9_39]
    [31] Zhou S, Wang JB, Xue PP, Wang XY, Kong L. An approach to the state explosion problem: SOPC case study. Electronics, 2023, 12(24): 4987.
    [32] Shen LX, Mu DJ, Cao G, Qin MY, Zhu JC, Hu W. Accelerating hardware security verification and vulnerability detection through state space reduction. Computers & Security, 2021, 103: 102167.
    [33] Jin Z. Environment Modeling-based Requirements Engineering for Software Intensive Systems. San Francisco: Morgan Kaufmann, 2018. [doi: 10.1016/C2014-0-00030-5]
    [34] Li WB, Hayes JH, Truszczyński M. Temporal action language (TAL): A controlled language for consistency checking of natural language temporal requirements: (Preliminary results). In: Proc. of the 4th Int’l Symp. on NASA Formal Methods. Norfolk: Springer, 2012. 162–167. [doi: 10.1007/978-3-642-28891-3_16]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

杨晓,王小齐,陈小红,金芝.复杂嵌入式系统需求一致性的组合验证方法.软件学报,2025,36(4):1413-1434

复制
分享
文章指标
  • 点击次数:947
  • 下载次数: 2248
  • HTML阅读次数: 360
  • 引用次数: 0
历史
  • 收稿日期:2023-12-31
  • 最后修改日期:2024-02-20
  • 在线发布日期: 2024-07-03
  • 出版日期: 2025-04-06
文章二维码
您是第20381094位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号