Nuttx操作系统进程切换调度实时性的形式化验证

摘要

随着工业机器人的发展,实时性操作系统在工业控制领域的地位越来越重要.实时调度对实时操作系统的实时性有重要影响,是提高系统实时性的关键技术.Nuttx操作系统就是一个实时操作系统,它有三种调度策略:先来先服务、时间片轮转法以及零星调度.首次提出对以上三种调度策略进行切换,使得任务到达时能够根据自身的特点去选择适合自己的调度策略,以便得到更快的响应.对切换策略建立时间自动机模型;用计算树逻辑公式对实时性进行了形式化描述;在模型检测工具时间自动机Uppaal中进行了验证.结果表明该切换策略能够使任务在规定的时间内更好地完成操作,满足了系统的实时性.