Model checking real-time systems is complex, and requires a careful trade-off between including enough detail to be useful and not too much detail to avoid state explosion. This work exploits variability of the formal model being analysed and the requirements being checked, to facilitate the model-checking of variations of real-time specifications. This work results from the collaboration between academics and Alstom, a railway company with a concrete use-case, in the context of the VALU3S European project. The configuration of the variability of the formal specifications is described in MS Excel spreadsheets with a particular structure, making it easy to use also by developers. These spreadsheets are processed automatically by our prototype tool that generates instances and runs the model checker. We propose the extension of our previous work by exploiting analysis over valid combination of features, while preserving the simplicity of a spreadsheet-based interface with the model checker.

翻译：实时系统模型检测具有复杂性，需要在包含足够细节以保证实用性与避免过多细节引发状态爆炸之间谨慎权衡。本研究通过利用被分析形式化模型与被检验需求的变异性，促进了实时规范变体的模型检测。该工作源于学术界与铁路企业阿尔斯通（Alstom）在VALU3S欧洲项目框架下的合作，依托具体应用场景展开。形式化规范的变体配置通过具有特定结构的MS Excel电子表格实现，便于开发人员使用。这些电子表格由我们开发的原型工具自动处理，该工具生成实例并运行模型检测器。在保留基于电子表格的模型检测器交互界面简洁性的前提下，我们通过扩展特征有效组合的分析方法，对先前工作进行了改进。