One of today’s challenges is producing reliable software in the face of an increasing number of interacting components. Our system CHET lets developers define specifications describing how a component should be used and checks these specifications in real Java systems. Unlike previous systems, CHET is able to check a wide range of complex conditions in large software systems without programmer intervention. This paper explores the specification techniques that are used in CHET and how they are able handle the types of specifications needed to accurately model and automatically identify component checks. Categories and Subject Descriptors D. Software; D.2 SOFTWARE ENGINEERING; D.2.4 Software/Program Verification; Subjects: Model checking; Programming by contract. General Terms Verification, Design, Experimentation, Languages. Keywords Components, verification, specifications, flow analysis, finitestate automata.
Steven P. Reiss