Checking Event-Based Specifications in Java Systems |
| |
Authors: | Steven P Reiss |
| |
Affiliation: | Department of Computer Science, Brown University, Providence, RI 02912 USA |
| |
Abstract: | 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. CHET is able to check a wide range of complex conditions in large software systems without programmer intervention. It does this by doing a complete and detailed flow analysis of the software and using this analysis to build a simpler, model program. This paper explores the motivations for CHET, the specification techniques that are used, and the methodology used in statically checking that the specifications are obeyed in a system. |
| |
Keywords: | Specifications model checking flow analysis finite-state properties component usage |
本文献已被 ScienceDirect 等数据库收录! |
|