Compositional Prediction of Timed Behaviour for Process Control Architecture

摘要

The timing of properties is an essential consideration in the design, implementation and maintenance of embedded software development. In this paper, we present an approach to the prediction of timed and probabilistic nonfunctional properties of process control architectures. Our approach involves a novel compositional approach to model checking of statements in Probabilistic Computational Tree Logic (PCTL).