Compositional Techniques for Verification and Performance Analysis of Reactive Probabilistic Systems

Suny At Stony Brook, Stony Brook NY

Investigators

Abstract

CCR-9988155 Stark, Eugene W. Smolka, Scott A. State University of New York at Stony Brook "Compositional Techniques for Verification and Performance Analysis of Reactive, Probabilistic Systems" The research proposed here has as its objectives: (1) to develop significantly improved techniques for the formal specification, verification, and performance analysis of systems that exhibit concurrent, reactive, probabilistic, and real-time behavior; (2) to construct implementations of these techniques in the form of efficient computer-aided design tools; and (3) to assess these tools and techniques and guide their further development by applying them to problems drawn from actual real-world engineering practice. In this research, attention will be focused primarily on finite-state system models. A key characteristic of the approach is compositionality, which permits a large system to be described as the composition of a collection of simpler components and to be analyzed in a component-by-component fashion. This research will build on previous work of the PIs, in which they developed a model, called "probabilistic I/O automata" (PIOA), for the compositional specification of reactive, probabilistic systems, together with compositional performance analysis algorithms for this model. The proposed project would advance the state of the art in the area of formal specification and verification techniques for finite state systems, which holds promise for enabling more efficient production of more reliable software systems.