-
题名基于Spin的地铁门控制系统建模与验证
被引量：1
- 1
-
-
作者
舒新峰
张炎龙
孙林泽
-
机构
西安邮电大学计算机学院
-
出处
《西安邮电大学学报》
2015年第5期57-61,共5页
-
基金
国家自然科学基金资助项目(61050003)
陕西省教育厅自然科学基金资助项目(11JK1037)
-
文摘
针对地铁门控制系统(MDCS)安全问题,提出一种MDCS检测方法。通过分析MDCS的控制逻辑,使用Promela建立了基于Spin的MDCS系统模型,将MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验证性质,运行Spin后即可判断MDCS是否存在安全隐患。实验结果表明,该检测方法可有效验证MDCS的安全性。
-
关键词
地铁门控制系统
模型检测
SPIN
PROMELA
-
Keywords
metro door control system, model checking, Spin, Promela
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名承前启后 继往开来——开发“二程”讲学的文化资源
- 2
-
-
作者
孙林泽
-
出处
《娘子关》
2013年第3期56-58,共3页
-
文摘
一清代诗人王朝士题《程子岩》七律一首:攀萝蹑蹬入云峥,石室鸿儒说二程。雨过千峰悬墨迹,风来万岫响书声。紫霞护洞层层细,青草覆岩处处荣。启后承先光道脉,至今犹仰斗山横。盂县境内有座岩凹尖,山不在其高,但因"二程"讲学留下胜迹"程子岩"而闻其名。这首七律便印证了它的永不磨灭的千峰墨迹。
-
关键词
二程
伊川先生
侯仲良
千佛碑
识仁篇
程朱理学
郡君
文化遗址
清代诗人
宋代理学家
-
分类号
B244
[哲学宗教—中国哲学]
-
-
题名诗联的主题与文体
- 3
-
-
作者
孙林泽
-
出处
《娘子关》
2011年第2期56-57,共2页
-
文摘
一"文以载道",语岀北宋周敦颐《通书·文辞》:"文所以载道也。"也可以理解为"文"为文体,"道"为主题。当然,"文以载道"在不同的社会和各个不同的历史时期,打上了鲜明的阶级与政治的烙印。"文以载道"诞生在北宋时期,所谓"道"的准则,当然是封建伦理道德。漫长的封建社会之"道"与新中国社会主义之"道"不可同日而语,这是不言而喻的。
-
关键词
诗联
文体
载道
楹联
主题
爱国主义
格律诗
中国社会主义
封建伦理道德
古体诗
-
分类号
I207.6
[文学—中国文学]
-
-
题名动车飞(外一首)
- 4
-
-
作者
孙林泽
-
出处
《娘子关》
2010年第4期49-49,共1页
-
-
关键词
动车
高铁
神山
和谐
太行
柱架
展翅
锦绣
时空
正气
-
分类号
I227
[文学—中国文学]
-
-
题名诗二首
- 5
-
-
作者
孙林泽
-
出处
《娘子关》
2009年第4期22-22,共1页
-
-
关键词
表率
人大代表
反腐倡廉
优生优育
抗震救灾
社区
和谐
雄鹰
锦绣
城镇
-
分类号
I227
[文学—中国文学]
-
-
题名律诗六首
- 6
-
-
作者
孙林泽
-
出处
《娘子关》
2008年第1期46-46,共1页
-
-
关键词
神山
南村
三晋
忠义
作家
阳泉
采风
高长虹
娘子关
龙舟水
-
分类号
I227
[文学—中国文学]
-
-
题名保持党员先进性教育感赋
- 7
-
-
作者
孙林泽
-
出处
《山西老年》
2005年第8期39-39,共1页
-
-
关键词
党员先进性教育
代表
兰考泡桐
践行
和谐
丰年
春风
清廉
原则
公仆
-
分类号
I227
[文学—中国文学]
-
