CAJ | 학술논문

基于形式化的需求验证技术是确保铁路安全苛求系统需求正确的有效手段，有效的组织和管理需求验证形成的安全例证是安全评估的关键。本文应用形式化语言Event-B方法对需求进行建模、分析和验证，能够发现潜在危险、提高系统安全性，同时结合GSN更高效地组织和管理E-vent-B提供的需求安全例证，增加安全例证的可信性和可阅读性，使论证逻辑更清晰、更适合安全审核和评估。
기우형식화적수구험증기술시학보철로안전가구계통수구정학적유효수단，유효적조직화관리수구험증형성적안전예증시안전평고적관건。본문응용형식화어언Event-B방법대수구진행건모、분석화험증，능구발현잠재위험、제고계통안전성，동시결합GSN경고효지조직화관리E-vent-B제공적수구안전예증，증가안전예증적가신성화가열독성，사론증라집경청석、경괄합안전심핵화평고。
Formal-based requirement verification techniques is one of the effective methods to ensure the correctness of requirement for the railway safety -critical system .Safety case with effective organization and man-agement is the key factor for safety assessment .In this paper , formal language Event -B was used to do the mod-eling, analysis and verification work for the requirement specification , which could locate the potential danger and improve system safety performance .Meanwhile combining GSN method , the process of obtaining and manag-ing safety cases could be more efficient , which greatly improved the credibility and readability , made the argu-ment logic more clear and consistent and helped to pass the verification and approval of safety assessment .