Page 27 - 《软件学报》2025年第4期

杨晓 等: 复杂嵌入式系统需求一致性的组合验证方法 1433

interlocking systems. In: Proc. of the 27th Int’l Requirements Engineering Conf. Jeju: IEEE, 2019. 308–318. [doi: 10.1109/RE.2019.
00040]
[4] 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). [doi: 10.3969/j.issn.1001-4632.2016.02.16]
[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] 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). [doi: 10.13238/j.issn.1004-2954.201704260003]
[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. [doi: 10.1016/j.scico.2022.102777]
[8] 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 [doi: 10.13328/j.cnki.jos.006861]
[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. [doi: 10.1002/smr.2558]
[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. [doi: 10.1016/j.scico.2020.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. [doi: 10.1109/TITS.
2023.3324022]
[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. [doi: 10.1007/978-3-030-03044-5]
[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. [doi: 10.29327/1298728.24-7]
[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. [doi: 10.1109/TITS.2018.2869633]
[18] 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 [doi: 10.13328/j.cnki.jos.005952]
[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. [doi: 10.1007/s10009-010-0145-y]
[23] Rudolph E, Graubmann P, Grabowski J. Tutorial on message sequence charts. Computer Networks and ISDN Systems, 1996, 28(12):
1629–1641. [doi: 10.1016/0169-7552(95)00122-0]
[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.