知识卡片
SASIM仿真方法的五种仿真特征
内容
仿真在软件架构领域的核心价值是让架构师能借助原型快速检测架构决策的不一致性、改善设计——面对多种可能的架构决策时,每个方案的利弊都能通过仿真被预测,架构师可以快速分析一次架构改动的影响,从而理解整个系统在时间、性能、行为方面的内涵。Henry等人提出的SASIM仿真方法没有另起炉灶开发专用仿真器,而是巧妙复用了成熟的模型检测工具SPIN:先用Charmy(一种架构详细规格说明与验证环境,能描述组件、连接件及其拓扑分布,用状态图和顺序图详述每个组件内部行为及组件间交互)描述软件架构,再通过经典的Charmy-to-Promela转化算法生成Promela代码,Promela代码交给SPIN做模型检测和仿真,最后把验证结果和仿真的文本输出重新转化回Charmy的顺序图和状态图原型——这个”外部仿真器+专用前端语言+结果回译”的三段式结构,避免了从零开发一款专用仿真器的巨大成本,是一种务实的工程复用思路。SASIM支持五种仿真特征,覆盖了从”完全旁观”到”完全自定义”的一整个光谱:随机仿真——设计者是旁观者,有多种可能性时随机选中一种,可以逐步观察也可以快速运行;交互仿真——每一步都高亮显示所有可能行为,由设计者选择走哪条路,特别适合帮助设计者建立对系统行为的理解和信心;顺序图导引下的仿真——设计者预先设计一个顺序图描述想要或不想要的行为,SASIM尝试重现这个交互过程,但不生成新的顺序图、只用来指导仿真走向;仿真和穷举验证——验证失败时生成反例,并直接以状态图和顺序图形式呈现,帮助理解模型检测器的输出;模型差异的仿真——把设计者预先定义的一系列交互序列作为输入,检验整个序列能否被重现,能重现说明模型与预期一致,重现不了则暴露出模型与设计意图之间存在的差异。这五种特征本质上是把”仿真”从单一的被动观察工具,扩展成了一整套可以主动验证、主动比对、主动定位差异的分析手段。