One OS是一个专注于 可靠性和简易可用 的小型实时系统。它通过采取 形式化方法 来确保系统的可靠性。所有的实时操作系统必备的功能它都具备，但是并不在此基础上提供更多可选组件以确保内核的精炼性。这样，得到的内核就是一个最小化的内核，可以很方便地对它进行形式化验证。同时，它还可以作为客户操作系统运行在虚拟机监视器上。
本系统比一个全功能系统的相比要小得多，而且理解起来应该也相对容易得多。即便本系统 仅仅包含了一个.C文件 ，它仍然提供了高效的内存管理，抗锯齿图形界面库和其他实用函数，并且这些功能的实现都不消耗任何额外的RAM！
传统的软件设计方法基于自然语言的思考、设计和描述，往往片面和模糊，极易引起误解。它也无法进行严格的检查，只能通过人的心智进行分析。基于 UML 等半形式化的方法采用一些相对清晰的图形化描述，一些工具也能自动生成代码框架并检查分析。以上两种方法在测试系统时，均是设计一系列用例对其进行测试，最多有结构化测试的参与。但是，它们都 无法保证系统中没有错误 ，均不适用于性命攸关的系统的分析和开发，因此我们需要更为严格的开发设计流程。完全的形式化方法则基于严格定义的数学概念和语言，可以开发自动化工具进行检查和分析。它把数学的严格性带入软件开发的各个阶段，通过严格的数学证明 保证系统中没有漏洞和错误 。
请参见此链接
