摘要
实时系统的建模与验证是实时系统开发过程中不可或缺的环节。由于目前业界中广泛使用的建模验证工具UPPAAL存在下载安装慢、拖拽控件不灵活且不支持多用户进行项目团队管理等弊端与局限性,在考虑UPPAAL缺点的同时结合实际应用需要,设计并实现基于B/S架构的实时系统的建模和验证工具。该工具通过浏览器即可访问,提供良好建模操作体验的同时支持多用户进行项目团队管理。使用该工具编辑运行具体实例,验证了实例系统的可达性、安全性等性质,获得了预期的正确结果,完成了该工具的功能测试。
Modeling and verification of real-time systems is an indispensable link in the development process of real-time systems.Due to the shortcomings and limitations of UPPAAL,a widely used modeling and verification tool in the industry,which is slow to download and install,inflexible to drag and drop controls,and does not support multi-user project team management,this article considered the shortcomings of UPPAAL and combined actual application needs,designed and implemented a modeling and verification tool for real-time systems based on B/S architecture.The tool could be accessed through a browser,providing a good modeling operation experience and supporting multi-user project team management.The tool was used to edit and run specific examples,verifying the reachability and security of the example system,obtaining the expected correct results,and completing the functional test of the tool.
作者
石安
张卓若
代立云
Shi An;Zhang Zhuoruo;Dai Liyun(Southwest University,Chongqing 400715,China)
出处
《计算机应用与软件》
北大核心
2022年第10期11-17,34,共8页
Computer Applications and Software
基金
国家自然科学基金项目(61802318,61672435,61811530327)。
关键词
实时系统
时间自动机
形式化验证
Real-time system
Timed automata
Formal verification
