Method for determining operational characteristics of a program
AssigneeTrusted Logic
InventorsEric Vetillard, Renaud Marlet
Life of this patent
Estimating the term…
Abstract
The inventive method for determining operational characteristics of a program includes a verification procedure involving the following stages: the first stage for expressing the operational characteristics of the program in the form of functions related to events producible during possible executions of the program, a second stage for simultaneously estimating, by program analysis, the program structure, the possible ways of execution and values used at different program points and the third stage for determining said characteristics by calculating associated functions by means of information extracted with the aid of the analysis.
Claims19
A method for determining the operational characteristics of a program, comprising a verification procedure comprising the following steps:
- a first step comprising:
- expressing the operational characteristics of the program as functions dealing with occurrences or sequences of occurrences of events occurring during executions of the program, said events being able to deal with particular operations, particular values of data, at particular program points and in particular states of the program;
- determining a level of precision with which these characteristics must be determined;
- determining a set of particular contexts of execution in which the program will always be executed;
- and
- determining operational specificities of a set of platforms on which the program will be executed;
- a second step of estimation, by program analysis, and in consideration of said level of precision, of said set of particular contexts of execution and of said operational specificities of platforms, of information relating to a structure of the program, execution paths of the program and to values of data, at various points of the execution paths and under different execution conditions, of states of the program and data handled by the program;
- and
- a third step for determining said operational characteristics, by means of the information extracted by said program analysis, by computation of said functions on the occurrences or particular sequences of occurrences of particular operations, dealing with particular values, at particular points of the program, in particular states of the program, for the set of execution paths determined by analysis.
Dependencies are inferred from the claim text.