Computer Science ›› 2017, Vol. 44 ›› Issue (12): 156-162.doi: 10.11896/j.issn.1002-137X.2017.12.030

Previous Articles     Next Articles

Real-time System Verification Approach Based on Observer Patterns

ZHAO He, HONG Mei, YANG Qiu-hui and GAO Wan-ling   

  • Online:2018-12-01 Published:2018-12-01

Abstract: The verification of complex real-time system is always high-profile.A common way to describe the verification properties is using temporal logic,and the way is complex and difficult for laypeople.Observer patterns is an additional subsystem.It can transform the complex verification properties into simple reachability problem.The use of observer patterns can avoid using complex verification algorithm.The observer patterns proposed by Etienne and Nouha Abid were applied to the real-time system,Train-Gate system.UPPAAL was used to construct the observer models according to some scenarios in Train-Gate.Comparative experiment was used to compare the verification result with and without observer patterns.The experiment result shows that the use of observer patterns and verification properties both can get correct results.And the use of observer patterns can save time and it’s easier to accept for laypeople.Therefore,the use of observer patterns is feasible in the real-time systems like Train-Gate verification.

Key words: Observer patterns,Real-time system,UPPAAL,Train-Gate,Model checking

[1] ALUR R,DILL D L.A theory of timed automata[J].Theoretical Computer Science,1994,126(2):183-235.
[2] ANDRE E.Observer patterns for real-time systems[C]∥18th International Conference on Engineering of Complex Computer Systems(ICECCS 2013).Singapore,2013:125-134.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!