交互系统的可视化形式化方法

交互系统日益普遍。许多例子充斥我们的日常生活：汽车、飞机、防御系统、电话交换系统、金融系统、国家政府等等。更贴近计算机科学，嵌入式系统和体系之系统（Systems of Systems）是交互系统的进一步例子。所有这些的共同点是某个“整体”由组成部分构成，这些部分相互交互。根据设计，这些交互是有意的，但成问题的是非预期交互。体系之系统文献使用术语“构成系统（constituent systems）”和“构成体（constituents）”指代相互交互的系统。此处遵循该做法。本文提出一种可视化形式化方法，Swim Lane Event-Driven Petri Nets，提议作为交互系统的基于模型的测试（MBT）的基础。在缺乏可用工具的情况下，该模型仅能支持基于模型的测试的离线形式。