GénéSyst：Génération d'un système de transitions étiquetées à partir d'une specécification Bévénementiel
GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel
摘要：
在正式开发中，最昂贵的错误来源和更难检测的错误是规格说明期间的错误。因此，形式化开发的第一步通常包括展示规范的所有行为的集合，例如使用自动机。从这个观察开始，许多研究都是关于从行为规范（如UML）生成B机器的。然而，不进行向后验证。这就是为什么，我们提出了GeneSyst工具，其目的是生成一个自动机描述至少所有的行为规范。细化步骤被认为是在所产生的SLTS子自动机出现。
英文摘要：
The most expensive source of errors and the more difficult to detect in a formal development is the error during specification. Hence, the first step in a formal development usually consists in exhibiting the set of all behaviors of the specification, for instance with an automaton. Starting from this observation, many researches are about the generation of a B machine from a behavioral specification, such as UML. However, no backward verification are done. This is why, we propose the GeneSyst tool, which aims at generating an automaton describing at least all behaviors of the specification. The refinement step is considered and appears as sub-automatons in the produced SLTS.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
