Informal Description

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.

« back  |  home  |  top ^