Title :
Protocol validation for large-scale applications
Author :
Lin, Fuchun Joseph ; Liu, Ming T.
Author_Institution :
AT&T Bell Lab., Naperville, IL, USA
Abstract :
A threefold strategy incorporating formal modeling, structural decomposition and functional abstraction, and reachability analysis is described, and the role of each part in managing complexity is examined. Formal modeling helps weed out extraneous detail so that later work on decomposition and abstraction is easier. Decomposition and abstraction help divide complexity into manageability parts that the reachability algorithm can solve. Examples of the use of each are given.<>
Keywords :
computational complexity; formal specification; program verification; protocols; complexity; formal modeling; functional abstraction; large-scale applications; manageability; reachability analysis; structural decomposition; threefold strategy; Application software; Bridges; Computer bugs; Explosions; Large-scale systems; Protocols; Reachability analysis; State-space methods; Testing;
Journal_Title :
Software, IEEE
