System for formally supervising communications
View Patent ↗A system is provided for formally monitoring communications of a set of specific applications of a platform. The system includes an acquisition module configured to acquire a formal model of a data stream describing the behaviour of a group of participants modelling the set of specific applications, and a communication specification describing software implementations implementing the applications modelled by the participants. The software implementations are configured to call up predetermined communication functions, and a monitoring module is configured to verify that a sequence for calling up the communication functions complies with the expected behaviour of the group of participants.
1 . A system for formally supervising communications of a set of concrete applications of a platform, the system comprising:
processing circuitry configured to
acquire a formal model of a data stream comprising a set of actors exchanging quantifiable information with each other through unidirectional communication channels, said formal model describing a behaviour of said set of actors modelling said set of concrete applications, and a communication specification describing software implementations implementing the applications modelled by said actors, said software implementations being configured to make calls to predetermined communication functions relating to a programming interface of said platform, and
verify that a sequence of calls to said communication functions is in accordance with an expected behaviour of said set of actors,
wherein the quantifiable information includes a statically specified amount of data to be received on an input channel, a statically specified amount of data to be produced on an output channel, and a time constraint indicating a required time period during which a process of receiving the statically specified amount of data on the input channel and producing the statically specified amount of data on the output channel is to be completed,
wherein the processing circuitry is configured to construct an automaton for each software implementation corresponding to an actor, each automaton comprising a set of states whose transition from one state to another is triggered by a call from the software implementation to one of said communication functions, said automaton relying on the behaviour expected by the formal model to trace the valid call sequences to said communication functions.
2 . The system according to claim 1 , wherein each automaton comprises a first part associated with the initialisation of the software implementation and a second part associated with the operation of the software implementation, the transition from a final state of said first part to an initial state of said second part being triggered when a synchronisation signal is received by the software implementation, indicating the execution of a concrete application.
3 . The system according to claim 1 , wherein the processing circuitry is configured to generate software elements configured to capture calls to communication functions and to make sure that the sequence of calls made upon executing a concrete application corresponds to the sequence defined by the automaton.
4 . The system according to claim 3 , wherein the software elements comprise an extended function for each of the communication functions, an input data deadline management function, and a current activation management function.
5 . The system according to claim 1 , wherein the communication specification is a specification of a service-oriented implementation.
6 . The system according to claim 1 , wherein the communication functions are service-oriented and comprise a service offering function, an interface publishing function, a published interface subscription function, an emitting function, a receiving function, a requesting function, and a processing function on an interface.
7 . The system according to claim 1 , wherein the formal model comprises a set of configuration data required for the implementation of said actors.
8 . The system according to claim 7 , wherein the configuration data further comprises for each of the actors: budget, initial delay, initial deadline, input deadline, default input policy, persistent/ephemeral indicator, and strict/relaxed indicator data.
9 . The system according to claim 1 , wherein the communication specification comprises links between software implementations and actors in the formal model.
10 . A real-time on-board equipment, designed using the supervisory system according to claim 1 , wherein said on-board equipment is configured to receive measurements specific to its environment and to deliver results actuating functional operations.
11 . The equipment according to claim 10 , wherein said equipment is an autonomous or non-autonomous vehicle of a land, rail, aerospace or naval type.
12 . A method for formally supervising communications of a set of concrete applications, the method comprising:
acquiring a formal model of a data stream comprising a set of actors exchanging quantifiable information with each other through unidirectional communication channels, said formal model describing a behaviour of a set of actors modelling said set of concrete applications, and a communication specification describing software implementations implementing the applications modelled by said actors, said software implementations being configured to make calls to predetermined communication functions relating to a programming interface of said platform, and
verifying that a sequence of calls to said communication functions is in accordance with an expected behaviour of said set of actors,
wherein the quantifiable information includes a statically specified amount of data to be received on an input channel, a statically specified amount of data to be produced on an output channel, and a time constraint indicating a required time period during which a process of receiving the statically specified amount of data on the input channel and producing the statically specified amount of data on the output channel is to be completed,
wherein the method includes constructing an automaton for each software implementation corresponding to an actor, each automaton comprising a set of states whose transition from one state to another is triggered by a call from the software implementation to one of said communication functions, said automaton relying on the behaviour expected by the formal model to trace the valid call sequences to said communication functions.