Verification of Liveness and Safety Properties of Behavioral Programs Using BPjs

This paper presents semantics, syntax, and tools for specification and verification of safety and liveness properties of behavioral programs. Verification is performed directly on program code, by traversing its transition system. Liveness properties are defined using “hot states”, in which scenarios are allowed to stay for a finite time, but not forever. Safety properties are defined using assertions which allow labeling program states as having violations, and by analyzing program states for deadlocks detection. The paper defines liveness violations with regards to specific program components and describes an approach for validating the absence of such violations is a system. The proposed approach is supported by BPjs, an open-source tool suite developed by the authors.