一种基于有限状态机的操作系统需求层形式化建模方法及装置

摘要

本发明提供了一种基于有限状态机的操作系统需求层形式化建模方法及装置，属于嵌入式操作系统领域。该方法响应于对操作系统需求层进行建模的请求，从操作系统功能模块数据库中，获取操作系统对应的多个功能模块、各功能模块对应的至少两种子状态及引起各功能模块子状态发生变化的至少一种操作，从而确定操作系统的系统状态及引起系统状态变化的触发事件；根据确定的系统状态及引起系统状态变化的触发事件，建立基于有限状态机的操作系统需求层形式化模型。本发明具有良好的复用性、适应性和灵活性，可以准确地描述操作系统的运行过程，为下一步形式化验证奠定基础，以便更早地发现是否有潜在的错误，有助于完成整个操作系统的形式化验证。