Compositional Branching-Time Measurements

Formal methods are used to increase the reliability of software and hardware systems. Methods such as model checking, verification and testing are used to search for design and coding errors, integrated in the process of system design. Beyond checking whether a system satisfies a particular specification, we may want to measure some of its quantitative properties. Earlier works on system measurements suggest extending model checking techniques to measure quantitative artifacts, based on weights associated with the transitions of a transition system. Other works allow counting while performing model checking or runtime verification. This paper presents a simple and efficient compositional measuring framework based on quantitative state testers. The framework allows combining multiple measures, such as distance and power consumption, using a variety of functions, such as min, max, and average. This supports calculation of interesting compound measures that quantitatively characterize a system's behavior.