关键词: 数据约束,实时系统,连续时间,MARTE,ZIA,模型检测

Abstract: Real-time systems with data constraints refer to computing systems both with time-bound and data variables constraints．Now there are few studies about the specification and verification of a unified model which connects discrete data constraints and continuous-time together．The article presented a ZIA specification based on continuous-time which not only has continuous-time constraints,but also has discrete data constraints and then gave its temporal logic．MARTE is a modeling specification of a UML profile in the field of embedded real-time systems．MARTE is widely used in industry,but studies about its model checking are few．The article proposed Z-MARTE by expanding Z on MARTE,and converted Z-MARTE to a ZIA model based on continuous-time．When model checking for ZIA model based on continuous-time is realized,model checking for Z-MARTE is realized．Finally,an example was given to indicate that this method is feasible and effective.

Key words: Data constraints,Real-time system,Continuous-time,MARTE,ZIA,Model checking