Research on verification of behavior requirement patterns based on action sequences

Abstract

Function behavior requirements（FBR） and safety behavior requirements（SBR） were described by action se-quences.Compared with the traditional logic or graphic form,action sequences can express the temporal relationship among interactive behaviors more exactly.Moreover,FBR pattern and SBR pattern are constructed by action sequences,and the operation semantics of these patterns are also given.To implement the requirement verification based on behavior patterns,the necessary and sufficient conditions as well as the checking algorithm for the satisfiability of FBR pattern and SBR pattern are presented and proven by redefining the property expression and combination operation of LTS’s safety and liveness.The framework has been widely applied in the formal verification ＆ validation of component-based CTCS2/3 systems,and has shown great theoretical and practical significance to combinational verification of Compo-nent-based safety-critical systems.

Keywords

• safety-critical system;action sequence;behavioral requirement pattern;labeled transition system;pattern verification