首页>
外国专利>
Method for verifying safety properties of java byte code programs
Method for verifying safety properties of java byte code programs
展开▼
机译:验证java字节码程序安全性的方法
展开▼
页面导航
摘要
著录项
相似文献
摘要
In a method for verifying the safety properties of Java byte code programs, the functioning of the byte code program to be verified is modeled on a finite state transition system M, and the state space of the Java Virtual Machine (JVM) on a finite set of states in M. Once entered into a model checker, the data of finite state transition system M are compared to the data entered in the model checker as conditional set S to determine properties characterizing an acceptable byte code program. The byte code program to be checked is released for further processing only when the state transition system M fulfills all conditions of conditional set S.
展开▼