一种实时系统时间约束验证方法研究

摘要

Nowadays ,functional modeling and time constraint analysis are separated for safety-critical software in com-plex embedded system ,in the areas of automotive electronics .These systems as real-time systems should be ensured that they are accurate and can be analyzed by time constraint .Clock Constraint Specification Language (CCSL) is the standard language for describing clock constraints in a standard description language of a real-time system .Time constraint of real-time system described by CCSL regular expression ;The transformation rules of CCSL basic elements to time automata basic elements are designed .Using UPPAAL ,we validate that the real-time system satisfies the corresponding time constraints by verifying and analyzing the converted automata model .%目前,能够对汽车电子领域中复杂嵌入式系统安全关键软件功能模和时间约束分析的方法尚在研究中,而这些系统作为实时控制系统,应该确保其具有准确的 、可分析的时间行为.时钟约束规范语言CCSL是实时系统的标准描述语言中描述时钟约束的规范语言.采用CCSL规范表达式描述实时系统时间约束;设计了CCSL基本元素到时间自动机基本元素的转换规则;使用时间自用机验证工具UPPAAL对转换得到的自动机模型进行验证分析,验证实时系统是否满足相应的时间约束.