Research on verification of behavior requirement patterns based on action sequences
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 c...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2011-01-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/74418254/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | 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. |
|---|---|
| ISSN: | 1000-436X |