|
| | | Analyzing AUTOC/AUTO (hybrid) automata: autoc2auto, auto2nbac, nbac2auto |
There is the possibility to specify a system under the form of a parallel product of hybrid automata communicating through channels carrying parameters, with a CSP semantics.
We designed actually 2 (closely related) automaton formats. AUTOC allows to specify parallel products of automata, and can be compiled into the AUTO format, which describes a single automaton. AUTO is the central format, which is directly translatable forth and back to NBAC format. The reason why we did not use an already existing format (like the HYTECH format, for instance) is because we offer more datatypes and more powerful expressions.
The tool autoc2auto performs a product of automata into a single automaton. The product is partly implicit, partly explicit, as specified in the AUTOC file. The tool auto2nbac translate a single hybrid automaton to a NBAC system , with possibly a verification goal. Once NBAC has performed his analysis, one can obtain an annotated AUTO file with the tool nbac2auto, which takes as inputs both the original AUTO file and the NBAC file delivered by NBAC.
The tool auto2nbac translate this auto format to nbac format.
|
| | | Analyzing AUTOC/AUTO (hybrid) automata: autoc2auto, auto2nbac, nbac2auto |