随着科学技术的快速发展,物联网技术已经应用于我们工作与生活中的方方面面。物联网设备的安全性和稳定性已经越来越被人们所重视。嵌入式操作系统作为物联网嵌入式设备的最基础软件,其重要性毋庸置疑。内核服务是操作系统提供的最基础功能服务,只有内核服务的安全性和正确性得到保证,操作系统才能够稳定的运行。设计高效安全的内核服务是构建一个优秀嵌入式操作系统的关键。编程模型作为操作系统的重要内核服务,会决定系统的调度运行策略和应用程序开发的灵活性。如何保证嵌入式操作系统提供的编程模型的正确性,是一个十分重要的工作。形式化方法能够有效地验证操作系统内核服务,EventB方法已经逐渐被认可是一种验证复杂系统的有效形式化方法。EventB方法采用自顶向下的开发策略,即初始需求经过重写得到重写需求,根据重写需求再设计精化策略,之后按照精化策略进行模型搭建工作。采用模型精化技术,在更深一层的模型中实现更具体的需求,最终得到满足所有需求的实现模型。内存分配是嵌入式操作系统所提供的最基础和重要的内核服务之一,内存分配又分为静态内存分配和动态内存分配。动态内存分配服务对嵌入式操作系统的性能有很大影响。如果内存分配的额外消耗过多,嵌入式操作系统就无法在有多个请求时提供稳定的服务。如果内存分配的执行效率不够高,嵌入式操作系统也无法在有限的时间内响应请求。这些问题如果发生在诸如交通和医疗等重要场合,则会产生严重后果。在日益复杂的物联网环境中,使用高效且低消耗的动态内存分配算法非常重要。本文的研究工作和贡献主要有:·提出并验证事件总线混合编程模型提出了事件总线混合编程模型。事件总线将多线程与发布-订阅模式结合在一起,实现了多线程与事件驱动两种编程模型。事件总线的优点是可以对系统程序的编程模式进行灵活配置以适应不同情况。本文使用Event-B方法对事件总线进行形式化建模与验证,并在每层模型中都完成了对其安全性与活性进行的证明。通过清晰的模型描述和细致的精化策略设计,整个工作的自动验证率达到了91%。·设计并开发DLSF动态内存分配算法提出了自适应组织内存管理资源的动态内存分配算法:DLSF。除了具有常数时间复杂的运行效率外,DLSF算法还可以根据实际工作负载与应用程序的运行情况重新调整系统配置。DLSF算法能在不同的嵌入式系统环境下充分利用内存资源,提高了内存分配的资源利用率与在资源稀缺情况下内存分配的成功率。