摘要
AADL近年来在嵌入式实时系统领域得到了广泛的应用,相对于其他语言能够更好地描述系统的非功能属性,同时支持系统软硬件建模,在基于模型驱动的开发方法下对系统进行建模和分析,用形式化的方法对系统的相关属性进行验证,从而可以在设计阶段发现错误,对保证系统的安全运行和开发效率的提高有着重要意义。对于验证AADL模型可调度性的问题,文中利用时间自动机理论,根据AADL调度模型和时间自动机模型的语义相似性,将AADL模型转换成时间自动机模型,并设计转换插件,通过Eclipse插件开发技术将其集成到AADL建模与分析工具OSATE中。最后在UPPAAL工具中对转换后的时间自动机模型进行模拟和验证,利用相关性质验证语句等价地对原模型的可调度性进行验证。
AADL has been widely used in embedded real-time system in recent years. Compared with other languages, it can better describe the system non functional attributes, and also support the software and hardware modeling of the system. AADL can model and analyze the system based on the model driven development method,and verify relevant properties using formal method. Error can be found in the design phase,and it has great signiftcance to ensure the safe operation of the system and improve the efficiency of development. For verifying AADL model scbedulability problem, according to the semantics similarity of AADL scheduling model and timed automata model,the theory of timed automata is used to convert AADL model to timed automata model, and integrate conversion plug-in into the AADL modeling and analysis tool OSATE through the development of Eclipse plug-in technology. Finally ,the converted timed automaton model in the UPPAAL tool is simulated and verified, using the related verification statement to verify the schedulability of the original model.
出处
《计算机技术与发展》
2016年第3期23-26,共4页
Computer Technology and Development
基金
国家"973"重点基础研究发展计划项目(2014CB744900)
