Control and data abstraction: the cornerstones of practical formal verification

• 1 January 2000
• journal article
• Published by Springer Nature in International Journal on Software Tools for Technology Transfer
• Vol. 2  (4) , 328-342
• https://doi.org/10.1007/s100090050040

Abstract

Keywords

• FORMAL VERICATION { LINEAR TEMPORAL LOGIC { DATA ABSTRACTION { CONTROL ABSTRACTION { NETWORK IN- VARIANT { MODEL CHECKING { SAFETY AND LIVENESS PROPERTY { WEAK AND STRONG FAIRNESS
• FORMAL VERIFICATION
• LINEAR TEMPORAL LOGIC
• MODEL CHECKING
• REACTIVE SYSTEM