Thumbnail
Access Restriction
Open

Author Mcmillan, K. L.
Source CiteSeerX
Content type Text
Publisher Springer
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Large Data Type ♦ Complex System ♦ Compositional Verification ♦ Fifo Buffer ♦ Uninterpreted Function ♦ Unbounded Size ♦ Formal Verification ♦ Compositional Model ♦ Temporal Case Splitting ♦ Fixed Finite Resource ♦ Compositional Reasoning ♦ Small Size ♦ Memory Address ♦ Infinite State System ♦ Proof Assistant ♦ Data Type Reduction ♦ Small Finite Type ♦ Unbounded Range ♦ Compositional Model Checking ♦ Large Data Array ♦ Small Fixed-size Array ♦ Novel Way
Description In CHARME
. Compositional model checking methods can be used to reduce the formal verification of a complex system to model checking problems of tractably small size. However, such techniques are difficult to apply to systems that have large data types, such as memory addresses, or large data arrays such as memories or FIFO buffers. They are also limited to the verification of systems with fixed finite resources. In this paper, a method of compositional verification is presented that uses the combination of temporal case splitting and data type reductions to reduce types of unbounded range to small finite types, and arrays of unbounded size to small fixed-size arrays. The method also supports the use of uninterpreted functions in a novel way, that allows model checking to be applied to systems with uninterpreted functions. These techniques are implemented in a proof assistant that also supports compositional reasoning and reductions via symmetry. Application of the method is illustrated...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1999-01-01