Ambient calculus-based modal logic model checking

Abstract

Ambient calculus-based modal logic model checking is disclosed. In one embodiment, a method receives a process for analysis against a formula, and outputs whether it satisfies the formula. In one embodiment, process analysis is conducted in a recursive manner. The process is normalized to determine whether the process comprises a single element. The process is partitioned to determine whether each component satisfies the formula. A plurality of names of the process is determined, and it is verified that a name exists for the formula that is unequal to any of the plurality. Each process sublocation is analyzed, as well as the spatial process reach.

1 . A computer-implemented method that facilitates ambient calculus-based modal logic model checking, comprising: 
 performing an analysis on an ambient calculus-based representation of a process with a formula that is represented via ambient calculus; and    outputting a result of the analysis that is utilized to facilitate determining whether the process satisfies the formula.    
   
   
       2 . The method of  claim 1 , the analysis comprises one or more of an ambient calculus-based initial check; an ambient calculus-based process normalization; an ambient calculus-based process partition; an ambient calculus-based process name determination; an ambient calculus-based process sub-location check; an ambient calculus-based process spatial reach check; and an ambient calculus-based recursive check.  
   
   
       3 . The method of  claim 1 , the analysis includes normalizing the process to determine whether the process comprises only a single element.  
   
   
       4 . The method of  claim 1 , the analysis includes partitioning the process to determine whether each component of the process satisfies the formula.  
   
   
       5 . The method of  claim 1 , the analysis includes determining process names and verifying a unique name exists for the formula.  
   
   
       6 . The method of  claim 5 , the verification is facilitated via utilization of a unification algorithm.  
   
   
       7 . The method of  claim 1 , the analysis includes checking process sub-locations with the formula.  
   
   
       8 . The method of  claim 1 , the analysis includes checking process spatial reach with the formula to determine whether the process has a finite spatial reach.  
   
   
       9 . The method of  claim 1 , the analysis includes a recursive check that determines whether the process satisfies the formula when enclosed in a surrounding ambient.  
   
   
       10 . The system of  claim 1 , the process is a restriction-free process, wherein for all restriction-free processes P and  -free closed formulas A, P A if and only if Check(P,A).  
   
   
       11 . The system of  claim 1 , the result is utilized to facilitate fiuther processing, including one or more of an analysis by a program, a rendering to a display, a conveyance to a printer, storage to a storage medium, moving the process out of an ambient, moving the process into an ambient, and replicating the process.  
   
   
       12 . A computer system that facilitates ambient calculus-based modal logic model checking, comprising: 
 a first component that receives a process for analysis, the process is transformed into an ambient calculus-based representation of the process;    a second component that analyzes the ambient calculus-based representation of the process with an ambient calculus-based representation of a formula via an ambient calculus-based modal logic model checking approach; and    a third component that provides a result of the analysis that includes information related to whether the process satisfies the formula.    
   
   
       13 . The system of  claim 12 , further comprising a component that performs an initial check with the process and formula representations.  
   
   
       14 . The system of  claim 12 , further comprising a component that normalizes the process representation to determine whether the process has only one element.  
   
   
       15 . The system of  claim 12 , further comprising a component that partitions the process representation to determine whether each component of the process satisfies the formula.  
   
   
       16 . The system of  claim 12 , further comprising a component that determines process names from the representation and verifies the formula has a unique name with respect to the process names.  
   
   
       17 . The system of  claim 12 , further comprising a component that checks process sub-locations with the formula.  
   
   
       18 . The system of  claim 12 , further comprising a component that checks process spatial reach with the formula to determine whether the process has a finite spatial reach.  
   
   
       19 . The system of  claim 12 , further comprising a component that recursively checks whether the process satisfies the formula when enclosed in a surrounding ambient.  
   
   
       20 . The system of  claim 12 , the result is displayed on a monitor, printed by a printer, further processed to generate another result, and/or stored in media.  
   
   
       21 . The system of  claim 12 , the process is a one of a thread, an applet, and an agent.  
   
   
       22 . The system of  claim 12 , the process comprises one or more sub-processes.  
   
   
       23 . The system of  claim 12 , the formula is a policy that is verified.  
   
   
       24 . The system of  claim 12 , the formula is a model that is checked.  
   
   
       25 . The system of  claim 12 , the formula is one of a security policy and a mobility policy.  
   
   
       26 . The system of  claim 12 , the formula describes how the process moves amongst various ambients.  
   
   
       27 . The system of  claim 12 , the formula provides how the process executes on a particular machine.  
   
   
       28 . The computer implemented method of  claim 1  comprises one or more programs that are stored on machine-readable medium and that are available for distribution, installation and/or execution on a computer.  
   
   
       29 . A method executed on a computer that facilitates model checking via ambient calculus-based modal logic, comprising: 
 matching a received process against a formula via ambient calculus; and    outputting whether the process satisfies the formula, based on the match, the output is utilized to facilitate execution of an action associated with the process.    
   
   
       30 . The method of  claim 29 , the action is one of a move out of an ambient, a move into an ambient, and a replicate.  
   
   
       31 . The method of  claim 29 , further comprising performing an initial check that includes at least one of the following ambient calculus-based checks: 
 Check(P,T)=T, which provides that the outcome of the analysis is T for any process when the formula is T;    Check(P, A)= Check(P,A), which means that if the formula is a negation  A, then the outcome of the analysis is the negation of a recursive analysis of the process P against formula A; and    Check(P,A B)=Check(P,A) Check(P,B), which means that the outcome of the analysis is the disjunction of recursively checking the process P against formula A and checking the process Q against formula B.    
   
   
       32 . The method of  claim 29 , further comprising normalizing the process when the formula is a location n[A].  
   
   
       33 . The method of  claim 29 , further comprising partitioning the process when the formula is a composition A|B.  
   
   
       34 . The method of  claim 29 , further comprising determining and verifying process names when the formula is an existential quantification ∃x.A.  
   
   
       35 . The method of  claim 29 , further comprising checking process sub-locations when the formula is a somewhere modality ♦A.  
   
   
       36 . The method of  claim 29 , further comprising checking process spatial reach when the formula is a sometime modality ⋄A.  
   
   
       37 . The method of  claim 29 , the further comprising recursive checking when the formula is a location adjunct A@n.  
   
   
       38 . A data packet transmitted between two or more computer components that facilitates model checking via ambient calculus-based modal logic, comprising: 
 an ambient calculus-based process that is analyzed against an ambient calculus-based formula, the analysis includes a model checking technique that facilitates determining whether the process satisfies the formula.    
   
   
       39 . A computer readable medium storing computer executable components that facilitate model checking via ambient calculus-based modal logic, comprising: 
 a component that analyzes a representation of a process based on an ambient calculus model checking approach; and    a component that outputs a result that indicates whether the process satisfies the formula.    
   
   
       40 . A system that facilitate model checking via ambient calculus-based modal logic, comprising: 
 means for representing a received process in an ambient calculus-based form;    means for comparing the ambient calculus-based form of the process with a formula represented in an ambient calculus-based form;    means for determining whether the process satisfies the formula; and    means for providing a corresponding result that facilitates handling the process.