Software systems have become an integral part of our lives. Today's
software systems are, however, highly error-prone, resulting in
disastrous results for users, and at times dire financial consequences
to the companies that own the software. It is now widely accepted
that formal verification is one of the most powerful tool we have to
gain a higher level of assurance in software.
Currently, most applications of formal verification focus on
``safety''. This, perhaps, is due to its importance in safety
critical systems, where, e.g., a ``bad'' state may cost human lives.
However, evaluating the quality of systems (or processes, or humans)
merely on what they *do not* do is hardly satisfactory. In fact, in
many cases, failing to respond to a request or to an urgent situation
may also have catastrophic consequences. Methodologically, it is
generally accepted that no specification can be complete unless it
contains both a safety and a liveness part.
Computer scientists draw different dividing lines between the classes
of "safety" and "liveness" properties. Some focus on the different
methodologies for their verification. Most (but not all) believe that
proving liveness properties is harder than proving safety properties.
Others do not see a clear (technical) dividing line and, consequently,
no need for special-purpose liveness tools.
Application experts typically require system specifications to
guarantee something good to happen (cf. use case specifications),
rather than the exclusion of misbehaviour. However, their
understanding of liveness can often be captured by methods drawn from
safety analysis. This is particularly true in the case of bounded
liveness, where the desired good behaviour must arise within a given
time bound. In fact, it is not always easy to convince applications
experts of the value of unbounded liveness.
The goal of the workshop is to bring together the main researchers in
the area of formal verification of software systems, representing
different approaches and methodologies, in order:
- study the essence of the safety/liveness spectrum
- attempt to agree on a common terminology for properties in the
spectrum;
- identify high priority objectives for future research, bearing in
mind "real-life" industrial problems.
As part of the workshop, a sample industry driven (infinite-state)
software system with specifications will be provided to the
participants, through which we may be able to develop a better
understanding of the merits of each approach and prospects of
integrating them.
