AUTOMATICALLY CLOSING OPEN REACTIVE PROGRAMS

We study in this paper the problem of analyzing implementations of ope n systems - systems in which only some of the components are present. We present an algorithm for automatically closing an open concurrent r eactive system with its most general environment, i.e., the environmen t that can provide any input at any time to the system. The result is a nondeterministic closed (i.e., self-executable) system which can exh ibit all the possible reactive behaviors of the original open system. These behaviors can then be analyzed using VeriSoft, an existing tool for systematically exploring the state spaces of closed systems compos ed of multiple (possibly nondeterministic) processes executing arbitra ry code. We have implemented the techniques introduced in this paper i n a prototype tool for automatically closing open programs written in the C programming language. We discuss preliminary experimental result s obtained with a large telephone-switching software application devel oped at Lucent Technologies.