Abstract:

Software is often being assembled using third-party components where the developers have little knowledge of, and even less control over, the internals of the components comprising the overall system. One obstacle to composing agents is that current formal methods are mainly concerned with “closed” systems that are built from the ground up. Such systems are fully under the control of the user. Hence, problems arising from ill-specified components can be resolved by a close inspection of the systems. When composing systems using “off-the-shelf” components, this is often no longer the case.

An off-the-shelf component one wants to use may not exactly match the user requirements, or it may be under specified. An under specification occurs when the specification of the component claims more behaviors than it actually has, some of which may render it useless. Given such an under-specified or mismatched module, we propose a method to automatically synthesize safety properties from it, that that can be used to tame its “bad” behaviors. The advantage of restricting to safety properties is that they are monitorable.

We present various methods for synthesizing such safety properties when the user specification and the component specification are given by automata or by temporal logic formulas. The safety properties are derived using an automata-theoretic approach. When restricting to omega-regular languages, there is no maximal safety property. We construct an increasing sequence of safety properties. We also show how to construct infinite-state automata that can capture any safety property that is contained in the original specifications.

Joint work with L. Zuck, M. Zhou et al.

A. Prasad Sistla obtained the PhD degree in computer science/applied mathematics from Harvard University in 1983. Prior to that, he obtained the ME degree in computer science from the Indian Institute of Science, Bangalore, India. He is currently a professor in the Department of Electrical Engineering and Computer Science at the University of Illinois at Chicago. Prof. Sistla has done extensive research in the areas of analysis and verification of concurrent systems, formal method for concurrent and distributed systems, and also in active and multimedia database systems. His current research interests include all of the above areas. Prof. Sistla has published extensively in leading computer science journals and conferences. He has served on the program committees of important computer science conferences. Prof. Sistla's research has been funded by leading organizations, such as the U.S. National Science Foundation, AFOSR, DARPA, etc.