摘要
实时系统必须在一个事先定义好的时间限制内对来自外部或内部的事件进行响应,如何有效验证实时模型的正确性和安全性是一个难点。文章通过多个时间自动机来模拟实时系统中的各个对象,并用UPPAAL对模型进行验证,减少了模型验证的状态搜索空间,为实时嵌入式系统开发和验证提供了一种可行、安全的控制机制。实验结果显示了系统的有效性。
Real-Time system is the system that must response the external or internal events in a pre-defined time.Certificating the security and reliability of the model is one of the difficult.This paper uses time-automata to simulate the objects in real-time system,and uses UPPAAL to verify the model.It can reduce the search of the state space;provide a feasible and safe control method for real-time embedded systems development and verification.Experiment shows that the method is effective.
出处
《计算机时代》
2011年第6期1-3,共3页
Computer Era
