用 SPARK 构建高完整性应用

Hacker News 上怎么说

• eggy · 2022 年

  ……被所有搜出来的 Apache Spark 玩意儿搞得很烦，不过过去这一两年这股风头似乎消退了点。佛蒙特技术学院（VTC）用 SPARK2014 来给他们的立方星（CubeSat）写程序，而《Building High Integrity Applications with SPARK》[1] 这本书就是很棒的入门教材，带入了很好的实战应用背景。AdaCore 官网上还有一篇文章，讲的是有人用 SPARK2014 重写了某些无人机的固件，这又是另一个很棒的真实世界……

  …annoyed by all of the Apache Spark stuff that came up, but that seems to have waned a bit this past year or two. Vermont Technical College (VTC) used SPARK2014 to program their CubeSat and the book, "Building High Integrity Applications with SPARK"[1] is a great intro to it in a nice context of practical use. There was also an article on the AdaCore site about someone who rewrote some drone firmware in SPARK2014, which is another nice real-world…

• eggy · 2022 年

  ……还得需要一段时间。Ada 在这个领域资历更老。我正在做安全关键型的控制系统，在 SPARK 和 Ada 这个领域，现有的很多成果都可以直接拿来用。这本名为《Building High Integrity Applications with SPARK》的书[2]真的让我彻底折服于它的优势。书中极好地介绍了 SPARK 如何应用于佛蒙特技术学院（VTC）的立方星项目。一颗立方星已在 2013 年成功发射。我没能找到任何……

  …going to be some time. Ada has a longer legacy in this game. I am working on safety critical control systems and there is a lot to prune from existing work in this area in SPARK and Ada. This book[2], "Building High Integrity Applications with SPARK" really sold me on the benefits. It is a great intro of how SPARK was used for the CubeSat program at Vermont Technical College (VTC). A CubeSat was successfully launched in 2013. I could not find any…

• pjmlp · 2021 年

  对，这里有几本关于它非常棒的书，考虑到主题尤其切题。《Building High Integrity Applications with SPARK》https://www.amazon.com/Building-High-Integrity-Applications-...《Building Parallel, Embedded, and Real-Time Applications with Ada》https://www.amazon.com/Building-Parallel-Embedded-Real-Time-...《Embedded…

  Yep, here some very good books about it, specially relevant given the main subject. "Building High Integrity Applications with SPARK" https://www.amazon.com/Building-High-Integrity-Applications-... "Building Parallel, Embedded, and Real-Time Applications with Ada" https://www.amazon.com/Building-Parallel-Embedded-Real-Time-... "Embedded…

• nickpsecurity · 2024 年

  《Building High Integrity Applications with SPARK》https://www.amazon.com/Building-High-Integrity-Applications-... 这本会比绝大多数关于形式化验证的著作实用得多。

  Building High Integrity Applications with SPARK https://www.amazon.com/Building-High-Integrity-Applications-... That will be more practical than most works on formal verification.

• tgv · 2026 年

  ……“白银”级别，也就是通过所有检查，更别提真正证明正确性的“黄金”级别了。上网搜 SPARK，剩下的内容几乎一片荒芜。我淘了一本 John W. McCormick 和 Peter C. Chapin 写的二手《Building High Integrity Applications with SPARK》。里面有完整的示例，概念解释得相当深入。可惜这书太贵了，因为我只是随便玩玩，就买了最便宜的……

  …"silver" level, where it passes all checks, let alone "gold", where you actually prove correctness. The rest of the internet is practically barren when you search for SPARK. I got a second-hand copy of Building High Integrity Applications with SPARK; John W. McCormick, Peter C. Chapin. It contains complete examples, and explains the concepts pretty much in depth. Unfortunately, the book is expensive, and since I was just dabbling, I got the cheapest,…

• pjmlp · 2017 年

  一本讲这方面的好书是《Building High Integrity Applications with SPARK》。http://www.cambridge.org/us/academic/subjects/computer-scien... Ada/SPARK 在语言层面上就定义了并行计算，也就是所谓的 task。

  A good book about is "Building High Integrity Applications with SPARK". http://www.cambridge.org/us/academic/subjects/computer-scien... Ada/SPARK has parallel computations defined at language level, known as tasks.

正在加载完整评论……