形式规格说明的工具辅助多方面分析（使用Alelier-B和ProB）
Tool-Assisted Multi-Facet Analysis of Formal Specifications (Using Alelier-B and ProB)
摘要：
软件系统的工具辅助分析和方便的指导实践的正式方法仍然是激励的挑战。本文将讨论这些挑战。本文从多个方面对形式规格说明进行了分析。B方法和Atelier-B工具用于形式规范、安全属性分析和改进。ProB工具用于补充模型检验的研究，它有助于发现错误，从而改善以前的规格。
英文摘要：
Tool-assisted analysis of software systems and convenient guides to practise the formal methods are still motivating challenges. This article addresses these challenges. We ex periment on analysing a formal specification from multiple aspects. The B method and the Atelier-B tool are used for formal specifications, for safety property analysis and for refinements. The ProB tool is used to supplement the study with model checking; it helps to discover errors and there fore to improve the former specifications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
