This is another one of those posts devoted to misc. things which may be of interest to readers of this blog. HVC The Haifa Verification Conference 2015 is upon us (Nov 16-19). If you are in Israel at that time and have nothing better to do, here are some reasons you might want to come … More Misc. stuff: HVC, game design languages and more
Summary: This post will dig into the verification challenges of autonomous systems, and especially into the challenge of verifying those which use machine learning. This post will discuss the verification of Intelligent Autonomous Systems (IAS) which have to interact with people and the outside world. Examples are AVs, UAVs, and autonomous robots of various kinds. … More Verification challenges of autonomous systems
Summary: This post explains why security research is relevant for this blog, and discusses three specific areas worth tracking. Hi folks – I’m back (vacations and all that). Security people deal with finding security issues (vulnerabilities) in systems. This blog deals with a different topic: big-system verification, where verification is defined as finding functional / … More Security research is pretty relevant for us
“Misc. stuff” posts will appear periodically. They will contain, well, miscellaneous [1] stuff – mainly links to papers and discussions which might be interesting to readers of this blog. For each, I’ll try to explain why it is relevant [2]. Hacker News and this blog My spec bugs post made it to the first page … More Misc. stuff – HN, machine learning and Jupyter
Summary: this post discusses the fact that different groups use different verification terminologies, explains why this is a problem, and suggests a common terminology page. One problem with verification is that it consists of multiple “verification tribes” or v-tribes, with different terminology and habits. There is the HW v-tribe, which I am coming from: We … More Terminology for multiple verification tribes
In a previous post I discussed verification vs. validation, and claimed that: This is a valuable distinction for a specific subsystem, but (in any complex system) this is a subsystem-relative concept, not an absolute one (as in “one man’s ceiling is another man’s floor”). I was reminded by some readers that this view (“real systems … More The soup of systems
Most bugs which kill people (and projects) are spec / requirements bugs, not implementation bugs. This could be a missing top-level requirement, a missing implication of some requirement on a lower-level spec, or some emergent behavior which was never spec’d. This post will explore the problem of spec bugs, and discuss possible solutions. Note that … More It’s the spec bugs that kill you
A companion post talks about spec bugs and ways to avoid them. Spec / requirement bugs (as opposed to implementation bugs) occur when the spec for a subsystem does not take into account some higher-level, full-system requirements. Spec bugs are pretty important, so here I’ll talk about some common verification-related concepts, and (my interpretation of) … More Terminology related to spec bugs
I started writing this blog mainly for feedback (see here), but did not know what to expect. Turns out I get good comments in the blog itself, but also (and unexpectedly) quite a few comments in private emails. Private emails are good, but not ideal (because you, gentle reader, don’t get to see them, and … More Some good comments I got lately about requirements
The topic of Formal Verification (FV) and how it relates to Coverage Driven Verification (CDV) came up in some previous posts and in a comment thread. So allow me to briefly discuss it – I promise to get back to the main course soon. Some definitions Before I continue, let me define what I mean by … More FV has much better PR than CDV