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

• 作者: 李晓娟 王瑞 郝英华
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 工业机器人 实时调度 Nuttx操作系统 切换 实时性 时间自动机Uppaal
• 年，卷（期）: 2018,（7）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 15-20,51
• 页数: 7页
• 分类号: TP316
• 字数: 3941字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2018.07.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李晓娟	首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室	39	261	9.0	14.0
2	王瑞	首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室	10	44	4.0	6.0
3	郝英华	首都师范大学信息工程学院	1	1	1.0	1.0