关键词：安全苛求系统 安全性分析 形式化方法 形式化验证 

摘要：采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。

计算机科学杂志要求:

{1}正文公式的序号一律靠右空两格，用(1)、(2)、(3)等表示。

{2}请勿一稿多投，三个月没有得到用稿通知，可自行处理。

{3}来稿一律文责自负。依照《著作权法》有关规定，本刊可对来稿做文字修改、删节及图像处理。凡有涉及原意的修改，则征求作者意见。修改稿逾3个月不寄回者，视作自动撤稿。

{4}标题序号按照“一”、“（一）”、“1”、“第一”或“首先”顺序排列，一般不用“①”号。根据文章具体内容，序号可适当减少，但不可反顺序使用。

{5}文末注明联系电话、详细单位地址邮编。

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社