Modeling a matrix for formal verification

Abstract

A reference model may be defined to refer to a matrix of a target computerized system. The reference model may comprise a reference index and a reference matrix. The reference index may have a non-deterministic value enabling the reference matrix to refer to the matrix using a fewer number of cells. The disclosed subject matter may enable a more efficient model checking process of a computerized device by using a reference model that is relatively easy to define or maintain or by using a reference model that is configured to be more efficient for model checking as it uses non-determinism.

1 .- 20 . (canceled) 
     
     
         21 . A computerized apparatus having a processor coupled to a memory, the processor being adapted to:
 obtain a specification of a matrix, the matrix has a first predetermined dimension, the matrix comprises one or more cells, each cell having a value, the specification comprises a transition relation defining transformation of a first state of the matrix to a second state of the matrix; and   generate, by the processor, a reference model of the matrix, wherein the reference model comprising: a reference index, the reference index associated with a non-deterministic value, a list of one or more cells associated with the reference index, the list and a value of the reference index are associated with a portion of the matrix, and an operation modifier for modifying an operation on the matrix to operate on the list, wherein the reference model preserves behavior defined by the specification.   
     
     
         22 . The computerized apparatus of  claim 21 , wherein the reference model comprises a fewer number of cells than the matrix. 
     
     
         23 . The computerized apparatus of  claim 21 , wherein the matrix is a sparse matrix. 
     
     
         24 . The computerized apparatus of  claim 21 , wherein the matrix is a two-dimensional array. 
     
     
         25 . The computerized apparatus of  claim 21 , wherein the matrix has more than two dimensions. 
     
     
         26 . The computerized apparatus of  claim 21 , wherein the specification further comprising a definition of one or more initial states. 
     
     
         27 . The computerized apparatus of  claim 21 , wherein the specification further comprising a behavior of an output variable. 
     
     
         28 . The computerized apparatus of  claim 21 , wherein the reference matrix is selected from a group consisting of a column in the matrix, a row in the matrix and a sub-matrix of the matrix having a predetermined dimension fixated. 
     
     
         29 . The computerized apparatus of  claim 21 , wherein a reference cell corresponds to a cell in the matrix having a row index, the row index is computed based on a row function, the row function provides a value based on a value of the reference index. 
     
     
         30 . The computerized apparatus of  claim 21 , wherein a reference cell corresponds to a cell in the matrix having a column index, the column index is computed based on a column function, the column function provides a value based on a value of the reference index. 
     
     
         31 . The computerized apparatus of  claim 30 , wherein the cell further having a row index, the row index is computed based on a row function, the row function provides a value based on a value selected from a group consisting of the reference index and the column index. 
     
     
         32 . The computerized apparatus of  claim 21 , wherein said processor is further configured to model check a model of the matrix with respect to the reference model. 
     
     
         33 . The computerized apparatus of  claim 21 , wherein model checking by said processor is comprised of: determining a property holding that a value of a portion of the matrix is equal to a corresponding value of a portion of the reference model; and utilizing a model checker to determine whether the property is held. 
     
     
         34 . The computerized apparatus of  claim 21 , wherein the portion of the matrix is selected from a group consisting of a row in the matrix and a column in the matrix. 
     
     
         35 . The computerized apparatus of  claim 21 , wherein said processor is further configured to obtain a specification property from a user. 
     
     
         36 . The computerized apparatus of  claim 21 , wherein the generation is based on user input selecting the portion of the matrix.