Method for assisting the development of a set of communicating automata

Method for assisting with the development of a set of communicating automata comprising a plurality of interfaces which process a plurality of interleaved messages, said automata being developed from interfaces external to the set, inter-automaton interfaces, the function that each automaton of the set must implement and the function to be implemented by the environment external to each interface external to the set, which method comprises the following stages:

• supplying to a development machine a description of initial elementary Petri nets respectively modeling partial behaviors of each function by describing events which fire or are consequences of transitions in each initial Petri net and assigning a label to each transition dependent on at least one event, each event firing or being a consequence of said transition, said events representing interfaces external to the set of automata, inter-automaton interfaces and interfaces between the initial Petri nets;
• verifying on said development machine that each initial Petri net has required properties;
• supplying to said development machine a description of constraints between initial Petri nets representing the behavior of the environment external to the set of automata;
• notifying to said development machine a plurality of Petri nets to be combined and a communication mode to cause it to combine initial Petri nets with each other or with modified Petri nets replacing initial Petri nets previously combined or to combine initial or modified Petri nets replacing initial Petri nets previously combined, each combination being effected by causing to communicate at least two initial or modified Petri nets using the labels of their transitions in the notified communication mode, which is chosen from the following modes:
• a synchronous mode;
• an asynchronous mode;
• a pseudo-synchronous mode in which events constituting communication with the environment external to the Petri net resulting from the combination are synchronous with the environment external to the Petri nets to be combined and asynchronous within the Petri nets to be combined, each pseudo-synchronous mode combination allowing for inter net constraints;
• causing said development machine to verify that the Petri net resulting from said combination has the required properties;
• supplying to the development machine a description of modified initial Petri nets replacing initial Petri nets to be combined if the Petri net obtained by combining the initial Petri nets does not have the required properties;
• and
• notifying again to said development machine a plurality of Petri nets to be combined and a communication mode to cause it to carry out a series of combinations and verifications until modified Petri nets are obtained having the required properties and respectively modeling each communication between two inter-automaton interfaces or between an external interface and the environment external to the set of automata and each automaton of the set.