Living safely

Let me warn you before I further talk about the $subject. It is from a technical point of view that I am looking at the $subject.

Have you ever thought what it would be like in real life to "live without safety" (e.g.: living in a zone where violence are frequent) or "be safe without actually living" (e.g.: living inside a cell at all times)? I am quite sure many of you have experienced one or the other, or at least heard about horrifying stories. No one would disagree with me that these scenarios are far from acceptable for any normal person. We ideally want both. We want to live and be safe (aka live safely).

It is no different in the technical world. I am referring to liveness and safety properties. "safety without liveness" will always hold as nothing happens to make it unsafe but there is little point having it in the first place (If a missile that is said to never miss the target is always safe so long as it is not fired - but what is the point of having it if it is not utilized). "liveness without safety" is dangerours as it may result in loss/damage to systems, people or other tangible and intangible items (what if there are traffic signals at a four way junction that turn green at the same time, what if there is an air traffic control system that allows two planes to land on the same run way, what if when you withdraw $20 from an ATM it goes on to deduct $200, and the like).

It took me some time to realize that every real problem specification is a combination of both liveness and safety properties. Some of the queries you might have are..

What does it actually mean that a system is safe or live? Do we have universal notions of them?
Do liveness and safety properties relace or complement one another?
Can we prove that every specification is a combination of both?
How do we prove a system is live or safe or both?
What does it mean that a program we have written is safe and/or live?
How do we identify safety or liveness bugs in a system?
What is the theoritical foundation for these properties?
Do these concepts relate to soundness and compleness?
and the list of questions goes on..

I will answer the above questions and more in another blog entry soon.