Most organizations want to produce systems that are safe, reliable, and secure. Most also realize that identifying these qualities is only a starting point.
To objectively verify whether a system has the required qualities, we must identify specific quality requirements. In ComFoRT, we encode these requirements as behavioral assertions.
Behavioral assertions are properties that can be expressed in terms of patterns of events (interactions) and state evaluations (e.g., values of variables or current mode of operation) and their relative ordering over time. Some examples of behavioral assertions are
These assertions are expressed in a state/event linear temporal logic (SE-LTL) developed specifically for ComFoRT. SE-LTL, unlike the logics used in many model checkers, allows behavioral assertions to be expressed in terms of both states and events—both of which are often important when describing desired properties of reactive software comprising many interacting parts (components).
To get ComFoRT, download the PACC Starter Kit from our Downloads page.