一种层次式时间自动机模型检测方法  

A MODEL DETECTION APPROACH FOR HIERARCHICAL TIMED AUTOMATA

作　　者：周宇[1,2] 胡军[1] 葛季栋[2] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210000 [2]南京大学软件新技术国家重点实验室,江苏南京210000

出　　处：《计算机应用与软件》2012年第11期48-51,共4页Computer Applications and Software

基　　金：国家自然科学基金项目(61100039);中央高校基本科研业务专项(NS2012135)

摘　　要：层次式时间自动机在软件系统建模过程中有着重要的应用。由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作。提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行。在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证。结合实时UML状态机图实例,证明了该方法的有效性。Hierarchical timed automata has important application in software system modelling.Due to the additional complexity introduced by the hierarchical nesting,direct formal verification is difficult to be carried out on it.In this paper we propose a flattening algorithm,which transforms the hierarchical timed automaton into a set of parallel sequential timed automata.Moreover,the concept of broadcast channel is employed to synchronise the execution of the sequential automata set.Based on this algorithm,a prototype is implemented,which can automatically transform the hierarchical timed automata to the input of a widely-used model checker UPPAAL so as to conduct the model verification.In conjunction of the example of real-time UML state-machine diagram,we prove the validity of our approach.

关 键 词：层次式时间自动机 形式化方法 模型检测 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]