Title
CafeOBJ as a tool for behavioral system verification
Abstract
We report on a machine supported method for verifying safety properties of dynamic systems based on the first-order description of underlying state transition systems. By capturing a set of states by a state predicate, we can verify safety properties of infinite-state systems using predicate calculus in the set-theoretic iterative calculation of least fixpoints.
Year
DOI
Venue
2002
10.1007/3-540-36532-X_26
ISSS
Keywords
Field
DocType
behavioral system verification,set-theoretic iterative calculation,underlying state transition system,infinite-state system,predicate calculus,verifying safety property,safety property,state predicate,first-order description,dynamic system,first order
Programming language,Computer science,Algorithm,First-order logic,Predicate (grammar),State transition systems,Dynamical system,System verification
Conference
Volume
ISSN
ISBN
2609
0302-9743
3-540-00708-3
Citations 
PageRank 
References 
3
0.41
6
Authors
2
Name
Order
Citations
PageRank
Akira Mori182.60
Kokichi Futatsugi2945111.37