Tool and method for designing and validating a data flow system by a formal model

Patent metadata

Field	Value
Publication number	US-11610041-B2
Application number	US-201917271964-A
Country	US
Kind code	B2
Filing date	Aug 30, 2019
Priority date	Aug 31, 2018
Publication date	Mar 21, 2023
Grant date	Mar 21, 2023

Abstract

The present invention concerns a method and a tool for designing and validating a data flow system comprising a set of software and/or hardware actors (ai, aj) interconnected with each other by unidirectional communication channels (ci, cj), the tool comprising: —a modelling interface (11) configured to generate an instance of the system by specifying, in a formal manner, a real-time and reconfigurable data flow, the reconfiguration of the data flow being carried out dynamically by propagating reconfiguration data from one actor to another through the communication channels, —an analysis module (13) configured to prove a predetermined set of behavioral properties of the system by means of a static analysis of the instance, —a refinement interface (15) designed to allocate resources to the instance, thus establishing a configured instance, the allocation of resources being carried out in such a way that an implementation of the system complies with the configured instance, and —a conformity test module (17) configured to verify the conformity of the behaviour of an implementation of the system with respect to the configured instance.

First claim

The invention claimed is:

1. A tool for designing and validating, implemented by a computer, a data flow system modelling an on-board device of a piece of equipment, said data flow system comprising a set of at least one of software and hardware actors interconnected with each other by a set of unidirectional communication channels, said tool comprising:
a modelling interface configured to generate an instance of said system by specifying a real-time and reconfigurable data flow, reconfiguration of the data flow being performed dynamically by propagating reconfiguration data from one actor of the actors to another actor of the actors through the set of unidirectional communication channels,
an analysis model configured to prove a predetermined set of behavioural properties of said system by a static analysis of said instance, comprising constructing a matrix defining an activation state of the actors and a state of the set of unidirectional communication channels, and determining a natural integer vector of which a product with the matrix is zero, the determining of said natural integer vector confirming feasibility of the data flow system independently of allocated resources,
a refinement interface configured to allocate the resources to said instance complying with said predetermined set of behavioural properties, to establish a configured instance, and
a conformity test module comprising unitary testing and integration tools, the unitary testing tool simulating a production of data on input channels of an implementation of a particular actor, and verifying that quantities consumed and produced by the implementation correspond to those specified for the particular actor, the integration test tool constructing a set of plots that correspond to an expected behaviour of the configured instance and ensuring that each plot provided belongs to a valid set to verify conformity of behaviour of the implementation of said system with respect to said configured instance.

2. The tool according to claim 1 , wherein the instance of the system comprises rational data consumption and emission rates.

3. The tool according to claim 1 , wherein the instance of the system comprises:
maximum frequency constraints for a certain actor of the actors, and
minimum frequency constraints fora certain other actor of the actors.

4. The tool according to claim 1 , wherein the instance of the system comprises:
the set of the at least one of software and hardware actors comprising generic actors configured to process data and mode actors configured to at least one of process data and select configuration modes,
the set of unidirectional communication channels connecting the set of the at least one of software and hardware actors with each other, each actor being associated with at least one input or output channel,
an integer or rational number of data produced or consumed by each of the at least one of software and hardware actors for each one of the input and output channels thereof, and
a set of modes associated with each of the mode actors, each of the mode actors being configured to dynamically choose, for each one the activations thereof, one and only one mode from among said set of modes.

5. The tool according to claim 4 , wherein the instance of the system comprises, for each of the generic actors, a corresponding set of execution modes, wherein the instance executes an implicit set of all other modes and passes, an execution mode that can either be a nominal mode common to an entirety of the system, or a specific mode chosen by a mode actor.

6. The tool according to claim 1 , wherein the instance of the system comprises an implicit set of feedback channels, a feedback channel, of the set of feedback channels, being a channel connecting a data-producing generic actor to a data-consuming generic actor, each executing in at least one of the modes, which is chosen by a same mode actor, and
wherein there is a path without repetition starting from said same mode actor and terminating by the data-producing generic actor by passing through the data-consuming generic actor.

7. The tool according to claim 1 , wherein the instance of the system comprises an initial state of the system composed by channel of a rational number and of a sequence of modes of a length equal to said rational number rounded down, and by a generic actor of the initial mode thereof.

8. The tool according to claim 1 , wherein said predetermined set of behavioural properties comprises:
a first property that verifies that resources required for implementation of communications between the actors without data loss are limited for a periodic execution of a specified system,
a second property that verifies that at least one of frequency and period constraints can be complied with without calling the first property into question,
a third property that verifies a non-existence of inter-blocking for any number of actor activations, and
a fourth property that verifies a non-existence of an unknown state in the system for all specified reconfigurations, and none of other of the properties being called into question by dynamic changes in configuration.

9. The tool according to claim 1 , wherein said system is a real-time on-board system of the piece of equipment, configured to receive measurements specific to said piece of equipment, and deliver results that actuate operations for a correct operation of said piece of equipment.

10. A real-time on-board system of the piece of equipment, comprising:
the set of the at least one of the software and the hardware actors interconnected with each other by the set of unidirectional communication channels, said on-board system being designed and validated by the tool according to claim 1 ,
wherein said real-time on-board system is configured to receive measurements specific to said piece of equipment and an environment thereof, and deliver results that actuate operations for correct operation of said equipment.

11. The system according to claim 10 , wherein said piece of equipment is an autonomous or non-autonomous vehicle of land, railroad, aerospace, or naval type.

12. A system of a real-time industrial process, designed and validated by the tool according to claim 1 , wherein said system is configured for industrial manufacturing of objects according to particular flow rate constraints and according to a reconfigurable process.

13. A method for designing and validating, implemented by a computer, a data flow system modelling an on-board device of a piece of equipment, said data flow system comprising a set of at least one of software and hardware actors interconnected with each other by unidirectional communication channels, said method using the computer to perform:
generating an instance of said system by specifying a real-time and reconfigurable data flow, reconfiguration of the data flow being performed dynamically by propagating reconfiguration data from one actor of the actors to another actor of the actors through the unidirectional communication channels,
proving a predetermined set of behavioural properties of said system by a static analysis of said instance, comprising constructing a matrix defining an activation state of the actors and a state of the unidirectional communication channels, and determining a natural integer vector of which a product with the matrix is zero, the determining of said natural integer vector confirming feasibility of the data flow system independently of allocated resources,
allocating the resources to said instance complying with said predetermined set of behavioural properties, to establish a configured instance,
simulating a pr

Assignees

• Commissariat Energie Atomique

Inventors

• Dubrulle Paul
• Louise Stephane
• Gaston Christophe
• Kosmatov Nikolay
• Jan Mathieu
• Lapitre Arnault

Classifications

• G06F17/16

  Matrix or vector computation {, e.g. matrix-matrix or matrix-vector multiplication, matrix factorization (matrix transposition G06F7/78)} · CPC title

• G06F30/00

  Computer-aided design [CAD] · CPC title

• G06F30/15 Primary

  Vehicle, aircraft or watercraft design · CPC title

• G06Q10/06313

  Resource planning in a project environment · CPC title

• G06F2111/04

  Constraint-based CAD · CPC title