使用UPPAAL进行模型检查:这是INSE 6250的课程项目。它专注于开发模型并使用任何模型检查器工具检查正确性 源码

INSE 6250-软件质量方法论(2020年冬季) 教授:贾马尔·本塔哈(Jamal Bentahar) 项目详情: 主题:使用UPPAAL进行模型检查。 将开发的模型:蒙特利尔地铁上基于Web的售票机。 模型检查器工具: UPPAAL [ ] 为了检查此模型的有效性,我想使用UPPAAL模型检查器,它是用于实时系统建模,验证和验证的集成工具环境。 抽象的 售票机是一种售票机,可生产纸质或电子票或为储值卡或智能卡或用户的移动钱包充值,通常在智能手机上。 例如,售票机在火车站分配火车票,在地铁站分配公交车票,在某些电车站提供电车票。 典型的交易由用户使用显示界面来选择票证的类型和数量