Most organizations want to produce systems that are safe, reliable, and secure. Most also realize that identifying these qualities is only a starting point.

• safe—for which operations or interactions, and in which situations?
• reliable—must the whole system be reliable or only critical elements of it? in the presence of what types of failures? what is the required up-time? what is the maximum period during which the system can be unresponsive?
• secure—with respect to what types of problems? information flow? coding errors? specific types of attacks?

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

• Industrial robots never enter a work area in which sensors indicate there is a person.
• Order acknowledgements are never lost or sent to the wrong receiver.
• Locked car doors can always be unlocked.

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).

Download ComFoRT

To get ComFoRT, download the PACC Starter Kit from our Downloads page.