We present a logic-based approach for analysing event-based requirements specifications
given in terms of a system’s reaction to events and safety properties. The approach uses an
event-based logic, called the Event Calculus, to represent such specifications declaratively.
Building on this formalism, the approach uses an abductive reasoning mechanism for
analysing safety properties. Given a system description and a safety property, the abductive
mechanism is able to identify a complete set of counterexamples (if any exist) of the
property in terms of symbolic “current” states and associated event-based transitions. If it
fails to find such an answer, this establishes the validity of the safety property with respect to
the system description. The approach is supported by a decision procedure that (i) always
terminates and (ii) facilitates analysis of this type of properties even in the presence of
incomplete domain knowledge, where initial conditions are not completely specified. A case
study of an automobile cruise control system specified in SCR is used to illustrate our
approach. The technique described is implemented using existing tools for abductive logic
programming.