博文
成也软件，忧也软件！111030
|||
到现在为止软件工程学并没有改变软件的尴尬境地，应用软件如此，系统软件更是如此，成也操作系统，败也操作系统。软件是信息技术系统产品的灵魂，带给人们财富，同时也带给人们灾难。严格软件开发方法的探索一直在进行，不同学术研究小组纷纷提出了自己的基于不同层面的验证方法与框架，试图提升软件的可验证性与可证实性，以此来保障软件的可靠运行。强化的条件约束与低效的灵活性是一对不可调和的矛盾主题。传统架构与方法的牢固现实束缚了新方法、新模式、新框架的落地生根，尽管验证的研究思路多样化，但真正落实到工程中的更是难上加难，造成落实难是多因素的。关系国际民生的特种软件研制有时也粗制滥造，形成用难，不用危险的两难境地。
从软件形成的各个环节与层面考虑，包括多方面的急需处理的难题，语言、语言处理、执行环境与操作系统的安全及可靠契合、外部环境因素的交互介入、系统的多层次验证与抽象等等。传统思想与工程观念要勇于革新，嫁接与抽丝同等重要。严格软件开发方法应首先在特种行业探索前行，比如列控系统的严格开发方法探索与实践，不论从严格的形式化验证入手，还是从工程环节入手，首先衡量的标准是管用，管用之后，经过反思会形成有效的学术与实践成果。
最近看到一篇文章《Advanced Development of Certified OS Kernels》，作者是耶鲁大学教授Zhong Shao与另外一名教授的文章，（中科大与耶鲁大学有个联合实验室，高可信软件构建方面的，Zhong Shao也参与其中）。气势宏伟，不过也做出了一些卓有见地的工作成果。
文中提到了Innovative Claims，三方面：
Clean-slate design and development of crash-proof kernels.
Programming languages for building end-to-end certified kernels.
Formal methods for automated analysis and proofs.
承前起后，确实思考与实践了这方面不少东西，感兴趣可以琢磨一下。
文章链接如下：ctos.pdf
https://blog.sciencenet.cn/blog-89075-502819.html
上一篇：IEEE ITSC2011关注论文主题
下一篇：可扩展高性能网络建模、模拟、分析工具集SSFNet
从软件形成的各个环节与层面考虑，包括多方面的急需处理的难题，语言、语言处理、执行环境与操作系统的安全及可靠契合、外部环境因素的交互介入、系统的多层次验证与抽象等等。传统思想与工程观念要勇于革新，嫁接与抽丝同等重要。严格软件开发方法应首先在特种行业探索前行，比如列控系统的严格开发方法探索与实践，不论从严格的形式化验证入手，还是从工程环节入手，首先衡量的标准是管用，管用之后，经过反思会形成有效的学术与实践成果。
最近看到一篇文章《Advanced Development of Certified OS Kernels》，作者是耶鲁大学教授Zhong Shao与另外一名教授的文章，（中科大与耶鲁大学有个联合实验室，高可信软件构建方面的，Zhong Shao也参与其中）。气势宏伟，不过也做出了一些卓有见地的工作成果。
文中提到了Innovative Claims，三方面：
Clean-slate design and development of crash-proof kernels.
Programming languages for building end-to-end certified kernels.
Formal methods for automated analysis and proofs.
承前起后，确实思考与实践了这方面不少东西，感兴趣可以琢磨一下。
文章链接如下：ctos.pdf
https://blog.sciencenet.cn/blog-89075-502819.html
上一篇：IEEE ITSC2011关注论文主题
下一篇：可扩展高性能网络建模、模拟、分析工具集SSFNet
扫一扫，分享此博文
全部作者的精选博文
全部作者的其他最新博文
全部精选博文导读
相关博文
- • 热烈祝贺海南大学9位学者入选斯坦福大学顶尖科学家2024年Career榜
- • 祝贺访问学者吕改芳和研究生杨梦蝶等合作SCI论文在Colloids and Surfaces A发表
- • Relativity of Hallucination（初学者版）
- • Are Human Beings Living in a Hallucination?(初学者版)
- • Theory of Relativity of Hallucination by Yucong Duan(初学者版)
- • The "Emergence" of LLMs by Relativity of Consciousness(初学者版)