摘要：自动检测与验证HMSC(high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义,为此提出一种为HMSC模型进行自动检验的方法,并将其实现。利用转换规则为HMSC模型生成Promela检测语言,借助SPIN工具对需求进行验证。该方法不仅支持模型检测,同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具,通过一个实例展示其自动建模检测分析的效果,表明了其有效性和实用性。

摘要：曹保平作为目前中国犯罪悬疑片导演中领军人物,一向致力于运用商业化的电影叙事来讲述小人物的挣扎与执着,在他的电影中,商业的表皮之下是导演对于生活的观察、热爱与放大。本文试图运用电影叙事学的相关理论,阐述其电影语言中的艺术表达与商业价值,通过对其类型电影元素的混搭,多种叙事结构的尝试,带有导演个人哲学思辨性的人物形象设置等方面的剖析,初步探究在电影越来越商业化的今天,曹保平如何在把握市场的同时,坚持自己对人性、对现实、对社会的独特且不失风格化的表达。